This part discusses how to install the infrastructure and its components locally.
The sources for the web-based infrastructure are available from the CVS repository under mrg/progs/Demo/Demo/Htmls/pcc. Note that at the moment all these are on a branch called demo-y3. Thus the command to check out all sources, best into a directory on your web server, is:
cvs -d :ext:firstname.lastname@example.org:/group/project/mrg/src co -r demo-y4 mrg/progs/Demo/Htmls
Alternatively, you can download the latest bundle of the MRG infrastructure, and copy the subdirectory progs/Demo/Htmls/pcc to the html directory of your web server.
To configure the checked out sources, you have to create a file called configure.php in both pcc/producer and in pcc/consumer. Several examples exist already. Check configure-romulus.php for an example of the setup I am using on my laptop which runs Mandrake 10.0.
You also have to manually create several directories, that are used as working directories: pcc/producer/PCCtmp and pcc/consumer/PCCtmp. Make these directories and the files in directory consumer/PolicyCurrent world-writable. The consumer side configuration file should contain an entry pointing to the Isabelle heap image of the logic used to check the certificate. Preferably, this image is put into pcc/consumer/heaps. The currently used heap file is MRG and is available from the net.
The versions of Camelot compiler, (de-)functionaliser etc all must match the version for the MRG demo of year 4!
Details on how to download and install the Camelot compiler are available on the Camelot Web Page.
If you download a binary RPM, just issue the command rpm -ivhrpm-file. If you download a source bundle, unpack it with
tar xvfz tgz-file
cd Camelot-distrib/src make
Create a link to the top-level compiler and put it into your path, e.g.
ln -s camelot ~/bin
You should have the following software installed to compile and run Camelot programs:
JDK 1.4.xx (to run the generated class file)
Once you have installed the infrastructure in a directory of your web server, e.g. as $srvroot/mrg/pcc, load this web page into your browser, e.g. by opening the URL http://$hostname/mrg/pcc/index.php. On the first page you see, you can configure the infrastructure to use different machines as producer and consumer. Pick the default settings, of using the same machine in both roles by pressing configure. Then click on "Continue as Producer".
You will arrive at the top-level page of the code producer (green background). On the left hand side you have links to available example programs. Click at "InsSortW". You will arrive at a page showing the code for insertion sort. You can edit the code if you wish. You can perform 3 operations on the code: run the space inference; compile the code to Grail; compile the code to JVM. To see which heap consumption the analysis infers select "Space Inference" and click "Submit". You will arrive at a page summarising the analysis. The most important line is
sort : 0, iList[0|int,#,0] -> iList[0|int,#,0], 0;
Click on Click "Compile this File" to compile the program to JVM and also generate a certificate for the heap consumption inferred by the compiler. You will see a page that lists the files that have been generated by the compiler, and bundled into a JAR file, for transfer to the code consumer. Click on "Transmit Me" to send it to the producer.
A new window will pop up, running on the code consumer (blue background). The first page summarises the files extracted from the JAR file, and some files constructed by the consumer out of the information provided by the certificate. Some explanation on the main information incorporated in the certificate, and on the top level theorem that is proven follows. At the bottom of the page you will find a button "Launch Isabelle". Click this button to start the certificate check, by feeding the files into the Isabelle/HOL theorem prover.
A new window will pop up that records the output of the certificate check. If the check succeeds you should see a line
SUCCESS: Resource property proven