Step-indexed semantic models of types were proposed as an alternative to purely syntactic safety proofs using subject-reduction. Building upon the work by Appel and others, we introduce a generalized step-indexed model for the call-by-name lambda calculus. We also show how to prove type safety of general recursion in our call-by-name model.
http://arxiv.org/abs/1105.1985
I did some final work on OCamlJIT2, and compared the result to OCamlJIT. The performance measures are presented in the following tech report (skip straight to section 4 for the performance results):
http://arxiv.org/abs/1011.6223
In short: Performance measured on a P4 “Northwood” (no long mode, plain x86) 2.4GHz. OCamlJIT2 beats OCamlJIT by a factor of 1.1 to 2.0 in every benchmark, and - rather surprising - was even able to beat ocamlopt in the number crunching benchmark (probably an issue with the x86 backend of ocamlopt).
As mentioned by Xavier Leroy and others previously, we probably went as far as we could go in the direction of JITting the byte-code virtual machine, while preserving its general stack-based nature and instruction set. Moving even further means translating the byte-code to some intermediate form suitable for use with standard compilation techniques; but as we saw earlier, in an LLVM-based prototype, the compilation overhead increases dramatically and the benefit of JIT compilation vanishes.
Therefore, as suggested earlier, I’ll try to get my hands on the native top-level now (already contacted Alain for the emitter code). Additionally, the linear scan register allocation will be implemented by a student as part of his diploma thesis.
See the discussion on the Caml mailing list.
OCamlJit 2.0 is a new Just-In-Time engine for Objective Caml 3.12.0 on desktop processors
(x86/x86-64). It translates the OCaml byte-code used by the interpreter (ocamlrun and ocaml)
to x86/x86-64 native code on-demand and runs the generated native code instead of interpreting
the byte-code. It is designed to run with minimal compilation overhead (translating only what
is being executed, avoiding costly code generation and optimization techniques), while being
100% compatible with the byte-code runtime (including serialization and hashing of closures,
etc.).
OCamlJit 2.0 was specifically designed for desktop processors and is not really portable to anything else in its current shape, because the target audience are people using the interactive top-level and the byte-code interpreter for rapid prototyping/development (which is unlikely to happen on anything else but x86/x86-64). The implementation currently requires a system that adheres to the SysV ABI, which includes Linux, BSD, OS X, but excludes Win32/Win64 (patches/ideas are welcome). It was tested on Linux/x86 (Debian), Linux/amd64 (CentOS) and Mac OS X 10.6 (64bit). The x86 implementation requires SSE2 capable processors (otherwise it falls back to the byte-code interpreter), so it won’t speedup your OCaml programs running on 486 CPUs. :-)
OCamlJit 2.0 runs most benchmarks at 2-6 times faster than the byte-code interpreter. The interactive top-level benefits twice when used with the JIT engine:
A tech report describing a slightly earlier prototype and including performance measures of OCamlJit 2.0 on Mac OS X (64bit) is available at:
http://arxiv.org/abs/1011.1783
The source code is available from the Git repository (master branch) at:
Installation is similar to installation of Objective Caml, just run
$ ./configure -prefix /path/to/ocamljit2 [options]followed by
$ make world opt
$ make installThis will install a fully working Objective Caml 3.12.0 to /path/to/ocamljit2, where
/path/to/ocamljit2/bin/ocamlrun and /path/to/ocamljit2/lib/libcamlrun_shared.so include
the JIT engine in addition to the byte-code interpreter (fallback to the byte-code interpreter
is necessary for debugging with ocamldebug). The configure script prints a line indicating
whether the JIT engine is enabled or not (if not, it’ll be just a regular OCaml 3.12
installation).
See the discussion on the Caml mailing list, and the more recent work on OCamlJIT2.
Git Hooks provides a simple mechanism to manage hooks for several Git repositories in a unified and simple way. It allows you to install hook scripts in a central location and use them for your Git repositories.
You need CMake and GCC in order to build and install git-hooks. You will also need to have Git and Perl installed for the hooks to work properly. To build git-hooks run
$ cmake /path/to/git-hooks
$ makein a new directory (preferably, tho you may also run it from the source directory). Then, use
$ make installto install git-hooks. This will install git-hooks to /usr/local. You can
use ccmake to change the installation prefix. Below, we will assume that you installed
git-hooks to /usr/local.
To setup a repository using git-hooks, just use the repository template that ships with git-hooks.
$ mkdir myrepo.git
$ cd myrepo.git
$ git --bare init --template=/usr/local/share/git-hooks/template ...This will setup the new repository myrepo.git with git-hooks. Check the
sample config file that will be created for myrepo.git.
To migrate an existing repository to use git-hooks, you should first backup
your existing hook scripts. Then replace the hooks with the ones from
/usr/local/share/git-hooks/template/hooks. Afterwards, you should migrate
your previous hook scripts to global hook scripts used by git-hooks.
The git-hooks package includes several useful hooks, which can be configured
to your needs using git config settings in your repository (or even global
settings from /etc/gitconfig). The
/usr/local/share/git-hooks/template/config file provides a sample
configuration file.
Please see the hook scripts in /usr/local/share/git-hooks/*.d/ for the
various supported config settings.
It took me some time to figure out how to get
gitweb and (readonly) HTTP
transport working for public Git repositories using the same URL. So here’s my
Apache 2 configuration, it may save you some time. The configuration assumes
that your Git repositories are located under /srv/git and the
gitweb files are installed in /usr/share/gitweb with the
configuration file in /etc/gitweb.conf.
# Dumb transport clone URLs for public repositories
AliasMatch ^/git(/.*\.git)/HEAD$ /srv/git/$1/HEAD
AliasMatch ^/git(/.*\.git)/info(/.*)? /srv/git/$1/info$2
AliasMatch ^/git(/.*\.git)/objects(/.*)? /srv/git/$1/objects$2
AliasMatch ^/git(/.*\.git)/refs(/.*)? /srv/git/$1/refs$2
<Directory "/srv/git/*.git">
AllowOverride None
Options Indexes
<Limit GET POST OPTIONS>
Order allow,deny
Allow from all
</Limit>
<LimitExcept GET POST OPTIONS>
Order deny,allow
Deny from all
</LimitExcept>
</Directory>
# gitweb user interface
Alias /git /usr/share/gitweb
<Directory /usr/share/gitweb>
SetEnv GITWEB_CONFIG /etc/gitweb.conf
Options +ExecCGI
AddHandler cgi-script .cgi
DirectoryIndex gitweb.cgi
RewriteEngine on
RewriteCond %{REQUEST_FILENAME} !-f
RewriteCond %{REQUEST_FILENAME} !-d
RewriteRule ^.* /git/gitweb.cgi/$0 [L,PT]
</Directory>