Mobile Resource Guarantees
(MRG, project IST-2001-33149)

Edinburgh MRG site meetings

NB: Let's try to avoid using JCMB 4310 - the acoustics are terrible!

The meetings are listed in reverse chronological order, so you don't have to skip down to the end.

26th August 2004

Bartek gave a talk on entitled Probabilistically checkable proofs for MRG - an invesigation. The slides are in PDF format.

8 April 2004

We looked at

N. Shaylor, D. N. Simon and W. R. Bush. A Java Virtual Machine Architecture for Very Small Devices. ACM SIGPLAN Notices, 38(7), July 2003.

29 January 2004 (3pm, JCMB 2509)

EmBounded: Formally Bounded Computation for Real-Time Embedded Systems
Kevin Hammond, University of St Andrews

This (very informal) talk introduces work related to the Framework VI EmBounded Project proposal and the novel language Hume.

The EmBounded project aims to identify, quantify and certify resource-bounded code written in Hume, a domain-specific high-level programming language for real-time embedded systems. Hume has been designed as a virtual laboratory for testing ideas related to resource prediction, incorporating high-level language features including recursion, automatic memory management, exception handling and higher-order functions. It represents the first serious attempt to deal with hard real-time programming in a functionally-based notation, and is structured as a layered language, where each layer adds expressibility but loses some formal properties of decidability.

Using formal models of resource consumption as a basis, the EmBounded project would develop static analyses for time and space consumption of Hume programs and assess these against realistic applications for embedded systems, taken from real-time computer vision algorithms for autonomous vehicles. The work is novel in a number of ways: in introducing high-level programming for embedded systems; in applying strong cost models to recursive, higher-order program definitions; and in combining analyses of both source- and machine-code into a single framework. There are obvious connections with e.g. work that is being done in the context of the MRG project.

15 January 2004 (3pm, JCMB 2509)

27 November 2003 (3pm, JCMB 4310)

13 November 2003 (3pm, JCMB 2511)

Also, Kenneth has some recent interesting results from profiling Camelot that he'd like to present.

30 October 2003 (3pm, JCMB 4310)

Added after the meeting

Most of the discussion was about the upcoming Munich workshop.

Possible areas for progress reports:
byte code logic
certificate generation
small devices and other demonstrations (Kenneth, Stephen)
O'Camelot
threads for Camelot? (Stephen)
higher-order functions in Camelot? (Kenneth)

Short-term future (= until annual review):
certificate generation! Ideally, we should be able to demonstrate full PCC from Camelot to certified bytecode with certificate checking, for a small but non-trivial example.

Medium-term future (= last year of the project):
Planning what to do and what not to do
What about resources other than space? Parameter restrictions on system calls via refinement types?
Resource types for Java library methods?

Long-term future (= after MRG):
GC2 initiative, and brainstorming on MRG2 and possible resources and security IP (Don)
e-science applications
smart cards and small devices
real-time Java

General: We need generous breaks in between the talks.

9 October 2003 (3pm, JCMB 3315)

Added after the meeting

Large amounts of information about Java for small devices can be found at the Wireless Java Developers' homepage, where downloads for various MIDP tools are also available. A brief introduction to J2ME, CLDC and MIDP can be found here. The Camelot source code for the example which I demonstrated, together with the makefile, can be found in this directory. Compilation depends on various things being in specific locations (currently in my home directory), and will only succeed on machines on the network at Edinburgh. The easiest way to compile the program is to go to the subdirectory progs/Camelot/midp_examples/PrimeSieve of your CVS directory and type "make". [The makefile uses a copy of the Camelot compiler which is in my home directory. If you want to compile things manually then be sure to have an up-to-date copy of the Camelot compiler. An old version is installed on the DICE machines, so make sure that you're invoking your own copy.] Type "make sim2" to invoke the MIDP 2.0 simulator (including profiling) on the sieve example.

28 August 2003

14 August 2003

25 June 2003 (*** 12pm ***)

8 May 2003

Don: Request proposal (actually mainly Stephen), GC2 initiative
Ian: APPSEM and Oxford talks about MRG, paper for FGC workshop on Grail together with Kenneth and Lennart
David: bytecode logic work ongoing with Lennart and Hans-Wolfgang, not finished
Kenneth: added diamonds to Camelot, minus checking of linear use of diamonds
Lennart: see above
Michal: inference of separation assertions for Camelot (in Haskell)
Robert: type systems for LFPL
Nicholas: optimizations for Camelot

29 Apr 2003 (*** 11am, JCMB 4311 ***)

13 Mar 2003 (*** 2pm, JCMB 4310 ***)

6 Mar 2003

They'd like to stimulate some discussion around a few design issues, and describe the plan for the byte code logic, which was outlined in the minutes of the recent management meeting:

• Finish improved version of operational semantics. Need to look carefully at this at both sites
  
• Produce cut-down version of this (Toy Grail) that is suitable for experimentation and publications
  
• Bottom-up work: experiments with examples on operational semantics, aiming to formulate useful derived rules
  
• Top-down work: come up with a set of proof rules, check that it is sound and (using examples, with pencil-and-paper proofs) that it is usable

Added after the meeting

The slides are here.

6 Feb 2003 (*** JCMB 5310 ***)

16 Jan 2003 (*** JCMB 2511 ***)

Abstract: Formal verification of interesting properties of realistic languages can be a daunting and frustrating task, even more so if we're not working at the right level of abstraction. This means to me (not) utilizing a logical framework which, by offering automatic support for certain menial duties such as variable convention and the like, allows the user to concentrate on the mathematics of the problem. Furthermore, (conservative) extensions of your basic framework will take care of apparently more unwieldy language phenomena. A typical example is the linear refinement of the notion of hypothetical judgment which allows one to express most elegantly state-based computations.

Depending on interest and time, in this talk we will discuss some of the following logical framework extensions:

• A strict lambda-calculus, introduced to allow negation-less negation in frameworks such as Twelf, but with technical implications in proof irrelevance for example in the context of runtime code generation.
• How to combine higher-order syntax, (co)-induction and tactical theorem proving in a well-understood setting such as HOL and using this methodology to formally verify soundness and completeness of a very simple compiler for Mini-ML.
• With the same approach (namely the so-called Miller/Felty "2-levels"), formalize several linear specification logics, e.g. the higher-order logic equivalent of the Linear Logical Framework and its cousin the Ordered Logical Framework, and an analogous of Miller's "Forum" presentation of linear logic and use them to prove meta-theoretic properties of languages with computational effects, concurrency and stack-based computations.

18 Dec 2002

28 Nov 2002

27 Nov 2002

31 Oct 2002

17 Oct 2002

19 Sep 2002

29 Aug 2002

15 Aug 2002

Added after the meeting

Lennart's slides are available here.

12th July 2002 (*** Friday, 11am, JCMB 2511 ***)

SML.NET: Functional programming in a non-functional world

27 Jun 2002

Added after the meeting

Michal's slides are available here.

12 Jun 2002 (Wednesday! 2511 JCMB!)

Added after the meeting

Lennart's slides are available here.

Kenneth mentioned two papers by Xavier Leroy: Java bytecode verification: an overview and Bytecode verification on Java smart cards. In the second paper, he shows that Javacard class files can be efficiently verified on-card if certain restrictions are placed on the bytecode. These restrictions are (1), that the operand stack is empty at all branch instructions, and (2) that each local variable has a fixed type throughout a particular method; these requirements will automatically be satisfied by code produced from (lambda)Grail. (There's also a third condition requiring that all local variables are clear at method entry, but this has to be enforced by the VM).

29 May 2002 (Wednesday!)

Currently, no specific topic has been put on the agenda, so unless
anybody has a particular issue he would like to talk about, we will
have an open discussion on various issues which came up at the
kick-off workshop (bytecode logics, SpecialJ, polymorphism, ...).
Also, David may talk about the cvs repository.

For people who weren't at the MRG meeting today, summary of CVS usage is:

     cvs -d /home/mrg/src checkout mrg

As an example of sharing (re)sources with CVS, I've added some of my MRG style files for slides as well as sources for my talks to the CVS. The one to look at is in talks/ToyMRG/. Typing "make" here invokes an elaborate makefile mechanism with numerous useful tagets, e.g. "make view" and (but don't try it) "make pub". See etc/Makefile.slides for more hints. (You'll either love it or hate it).

16 May 2002

David will talk about some of the ideas and mechanisms underlying
Proof-carrying code (bearing in mind that one of the inventors,
Peter Lee, is visiting us next week).

See the bibliographies at:

 http://www.cs.berkeley.edu/~necula/papers.html#annotated
 http://www-2.cs.cmu.edu/~concert/main.html#Publications

Good preparatory reading might be the most recent paper, on
a certifying compiler for Java.

Here are the slides from David's talk. He recommended reading the paper Safe, Untrusted Agents using Proof-Carrying Code rather than the more recent one mentioned above: this is the paper that includes a brief example of PCC for resource bounds (reference details are in PCC bibliography linked above, or in CVS bib/pcc.bib).

2 May 2002

Ian, Kenneth and Lennart have a proposal for a new improved Grail
along the lines discussed at the last meeting.  It is a functional
view of existing Grail, based on lambda-JVM, with easy translations to
JVM and .NET and also in the other direction.  This would allow real
bytecode (e.g. JVM) to be downloaded, but for the attached proof to
refer to the Grail version of that code.

This language can be given an operational semantics as an imperative
language and another interpretation in a lambda calculus style.  Once
these are written down, it should be possible to prove that they are
consistent.

Here is a short paper on lambda JVM (C. League, V. Trifonov and
Z. Shao. Functional Java bytecode. Proc. 5th World Conf. on Systemics,
Cybernetics, and Informatics, 2001.)

Here is a slightly polished version of the note handed out at the meeting. The conclusion of the discussion seemed to be that this is a very promising direction. One thing that is still missing is the object model - this proposal is only about what goes inside methods.

18 Apr 2002

Our next MRG meeting will be today at 4-5.  Don is in Germany but we
will try to include him in the meeting using the new LFCS conference
telephone.  We had hoped to be able to try to phone Martin and Olha
but Olha is not available so we will postpone contacting Martin until
another meeting.

On the agenda today is the continuation of our discussion from the
previous meeting about JVM versus .NET versus something more abstract.
Before the meeting please read the document which Kenneth circulated.

There are some features of .NET that look attractive (for instance, structures on the stack and support for tail recursion) but for use as a basis for MRG we decided that these are outweighed by the difficulty of finding out technical details about the framework, the relative lack of previous work on formalization in comparison with JVM, and the fact that there is only one implementation with source code available (1.9 million lines). Translation into .NET from some other platform seems very feasible and preferable to basing everything on it.

There then seemed to be two rather independent choices to make. First, between (1) a JVM-style language where programs are a list of instructions, versus (2) a lambdaJVM-style language where programs have nested structure. Second, between (1) a plain subset of (lambda)JVM or (2) an enrichment thereof with a few additional features that will make our lives easier while posing no particular problem in the cost model and being easily translatable to JVM, JCVM and .NET (for instance, unions to support LFPL-style diamonds). Grail represents choices 1+1. We thought 1+1 and 2+2 made more sense than 1+2 or 2+1, and are tending towards 2+2. Kenneth agreed to try defining such a language.

28 Mar 2002

We will briefly discuss plans for a kickoff workshop during or
adjacent to the Informatics Jamboree in May.  (There is money in the
MRG budget to invite one non-EU expert to that meeting, if we want --
ideas welcome!  An obvious possibility would be Martin Abadi who is
giving the Milner lecture.)

Then Stephen will speak about the .NET platform and MSIL in relation
to the Java platform and Java byte code, see project deliverable D1d.

Kickoff workshop: We thought that a 1-day meeting should suffice, with possible overflow into separate individual discussion on a second day, and that a good day would be Wednesday 22 May; this is the day of the Milner lecture (starts at 4.30pm) and the day after Frank's viva. We have funding to invite one non-EU expert, and the first choice is somebody from the ConCert project at CMU; Don will make contact. A possible venue is the new e-science centre next to Old College. David will take care of local arrangements.

Stephen's slides and a bibliography are here.

14 Mar 2002

Lennart will be talking about progress on the cost model.

Lennart presented ideas about accounting for time and space, both abstractly (n object of kind k required, n instructions of kind k executed) and concretely (n bytes required, n microseconds spent), by adding to the existing operational semantics. Lennart's slides are here.

Stephen has designed a possible logo.

28 Feb 2002

Robert agreed last time to tell us about compilation of LFPL.

Olha has just sent a proposal for a high-level functional language
(see also appendices A and B.  The final version of Kenneth's paper
on the virtual machine platform (Grail) is also available.

There is information about work on LFPL on the resbnd web page.

We discussed how MRG can build on this work. An obvious connection is that the high-level language in MRG could be an extension of LFPL. Another connection is that the design of the language of assertions about resource-related properties should look at LFPL-generated code.

14 Feb 2002

Kenneth is about to distribute a document describing his proposed set
of JVM instructions.  Please have a look at it before the meeting.  I
would like to decide then whether to regard this as finished, subject
to later work requiring revision, or not.  [Our first deliverable!]

Kenneth should look at the JVM instructions generated by MLJ to see how the profile compares with that of the Java library.

The acronym OIL (Open Intermediate Language) has been retired in favour of GRAIL (Guaranteed Resource Accounting Intermediate Language) -- thanks to Robert for the proposal!

David needs to do something about organizing the kickoff workshop, which was to be joint with a TYPES event.

It would be nice to have a logo for the project. Artistically inclined people are urged to propose one.

31 Jan 2002

Lennart, who is working on task 1b (Cost model) will say something
about this.

Kenneth has posted a draft proposal for a set of JVM instructions here.
There are some choices and we might discuss these.

Teaching staff have been asked to propose MSc project topics with a
deadline of Friday 1 Feb.  Some proposals related to the MRG project
would probably be interesting for students and the free manpower they
contribute might be useful.  This is another topic for discussion;
please come with some ideas for projects.

We discussed machine purchase; look here for information. CO bottlenecks mean that we need to wait until summer before buying anything that they will support. For now, we decided to buy a minimal-size laptop for conference presentations etc., to be shared but managed by David and/or Ian.

We discussed MSc projects. Stephen is proposing:

• one on "just in time" compiling Java byte code to our JVM subset (christened OIL, for Open Intermediate Language)
• another on JIT compiling .NET bytecode (MSIL) to OIL.

• relevant to task 1d ("Investigate .NET as an alternative to JVM"), repeating some of the work we are doing e.g. on cost model and logic but for the platform we don't pick
• case studies, for task 1f ("Collect some representative examples");
• experiment with an interactive theorem prover for generating proofs in byte code logic, for task 2e ("Implement a theorem prover") on which nothing else depends
• encode VM semantics in a theorem prover and show that the byte code logic proof rules are sound, for task 2f, on which nothing else depends
• implement some optimisations in the compiler produced by task 3b, for task 3e ("Implement well-understood optimisations in the compiler"), on which dependencies are far in the future

Some links related to Lennart's talk about cost models:

• Resource Management in Java: Grzegorz Czajkowski and Thorsten von Eicken. JRes: A Resource Accounting Interface for Java. Proc. 13th Conf. on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA-98). ACM SIGPLAN Notices 33(10):21-35 (1998).
• Java Virtual Machines:
  • HotSpot
  • Jalapeno: Bowen Alpern et al. The Jalapeno Virtual Machine. IBM System Journal 39 (2000).
  • Connected Limited Device Configuration & KVM: see here and this subnode
• I also took some information from these slides but I don't have any bibliographic information (I came across it when I searched for "JVM cost model" in Google)
• a profiling tool called "hrpof" is part of the Java environment and may be useful if we want to relate our cost models to a JVM
• Since Thursday, I had a brief look at the JavaCard Specification. As was to be expected, even more features are eliminated:
  • no dynamic class loading
  • no garbage collection, no finalisation
  • no threads
  • no cloning of objects
  • limited access control (public, protected attributes etc)
  • different security management
  • no types char, double, float or long
  • only one-dimensional arrays
  • restrictions on standard library

17 Jan 2002

Kenneth, who is working on task 1a (Definition of virtual machine
platform) has agreed to say something about the instruction set of the
Java virtual machine.  There will probably be a few organizational
things to talk about as well.

If you are looking for some bedtime reading, have a look at

P. Hartel and L. Moreau. Formalizing the Safety of Java, the Java
Virtual Machine and Java Card. ACM Computing Surveys, to appear, 2001.
http://www.ub.utwente.nl/webdocs/ctit/1/00000050.pdf

The idea of using the videoconferencing facilities at EUCS to hold meetings together with the Munich group was raised, and Ian agreed to look into it.

Some tentative decisions: leave out all 64-bit data and floats - concentrate on integers. Include arrays. Don't need exceptions or instructions to handle "finally" construct.

Some links related to Kenneth's talk on the virtual machine platform:

• Sun's JVM specification is here. Here is (part of) a book about the JVM which is a bit less terse than the official specification. And here is list of the JVM opcodes by category, rather than just alphabetically. This makes it a lot easier to work out what's going on.
• Information about the Waba virtual machine (a small JVM aimed at portable devices) is here and here.