Developers Guide

Installing the PCC Infrastructure

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:a1hloidl@ssh.inf.ed.ac.uk:/group/project/mrg/src co -r demo-y4 mrg/progs/Demo/Htmls

(adjust the username in the access string).

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!

Testing the Infrastructure

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;

which tells you that this is an in-place sort. This is achieved by the @_ annotation in the source code. See the Gentle Introduction to Camelot for more details.

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

at the bottom of the screen, followed by a report on the elapsed time. For the file InsSortW.cmlt the check should take about 10 seconds on a modern workstation. After this line you'll find a text field to supply input to the program and a button for executing the program. If you execute it, the results will pop-up in a new window. If the check does not succeed, you'll see a STOP sign.