The List-machine Benchmark

Version 2.1, May 2008

http://www.cs.princeton.edu/~appel/listmachine/2.0/

DOWNLOAD: listmach-2.1.tgz
DOWNLOAD: listmach.tgz (version 2.0)

SYNOPSIS: Build using "make".

LICENSE: Gnu Public License, version 3

Introduction

The original list-machine benchmark was introduced by Appel and Leroy [1] as a benchmark system for comparing proofs about Typed Assembly Languages (TALs). It is designed to be just complicated enough to make the proofs interesting. Much as the POPLmark challenge is intended to provide a framework for comparing proofs and proof systems involving typed lambda calculi, the list-machine benchmark is hoped to provide the same framework for TALs. The original release comprised, the list-machine 1.0 specification, a solution in Twelf, and a solution in Coq. This supported the comparison of two proofs done in a similar (proof-theoretic) style in two different proof assistants.

In this update to the list-machine benchmark, we explore the consequences of moving along a different axis in the proof space. Now we fix the proof assistant, Coq, and construct soundness proofs using a proof-theoretic technique (induction over typing derivations, etc) as well as a semantic technique [2,3].

In addition to our syntactic and semantic solutions (available above at DOWNLOAD), Adam Chlipala has contributed an alternate semantic solution using his Lambda-Tamer tactics. (This solution is based on the 2.0 release of the list-machine benchmark).

Changes to the list-machine itself

The 2.x branch of the list-machine benchmark features a slightly more powerful operational semantics. The 1.0 version of the list- machine had two control flow instructions: a direct "jump to label" instruction and a conditional jump that jumps when a value is nil. The 2.x list-machine also has two control flow instructions, and adds a data instruction. The new data instruction is the "load label" instruction, which loads and immediate label value into a register. An indirect "jump to register" instruction replaces the old "jump to label" instruction, and the conditional jump now tests for the distinguished label 0 rather than nil.

We extended the list-machine semantics because we wished to explore the consequences of indirect jumps. The richer programming model allows us to directly express nontrivial calling conventions and programs involving first-class functions, which was impossible using the original list-machine.

This change necessitates changes to the typechecking algorithm as well. In the 2.0 release, we demonstrated only a simple typechecker that has the same power as the original list-machine typechecker. We achieve this by only typechecking the instruction sequence where a label load to a register is immediately followed by an indirect jump to that register. In the 2.1 release, we have made a slight change to this typechecker to allow the loading of the distinguished 0 label to create a "nil" value (without this relaxation, no interesting programs will typecheck).

First Class Continuations: Also for the 2.1 release, we have added an "advanced" typechecker that allows the unrestricted use of label values. Labels are typed via a new "continuation type." The continuation type contains a type environment where the meaning is that it is safe to jump to the underlying label if the current register bank satisfies the continuation's type environment. Because the continuation type contains a finite map and is contravariant, it causes a moderate increase of complexity in the typechecking algorithm and its safety proof.

Proof Organization

The proof soundness for the simple typechecker is organized roughly as follows (the numbers are for easy reference). Solid boxes represent concrete implementations, and dashed boxes (i.e. box #4) represent specifications. Single arrows represent dependencies, and double arrows represent specification implementation. The advanced typechecker proof has exactly the same organization, except that the advanced typechecker currently lacks a syntactic proof; the development files simply have the prefix "advanced" rather than "simple".

                +- #9 ---------+   +- #6 ---------+
                |  Semantic    |   |  Syntactic   |<----- (from #2)
                |   Soundness  |   |   Soundness  |
                +--------------+   +--------------+
                 ^         ||          ||
                /          ||          ||
   +- #8 ---------+        ||          ||
   | List-machine |        ||          ||
   |  Hoare Logic |        ||          ||
   +--------------+        ||          ||
          ^                \/          \/         +- #5 ---------+
          |              +- #4  - - - - - +       | Simple TC    |
    +- #7 -------+       | Simple TC Spec |------>|    Soundness |
    |  Semantic  |<      + - - - - - - - -+       +--------------+
    |   Program  | \          ^                       ^
    |    Logic   |  \         |                      /
    +------------+   \        |                     /
                      \+- #2 ------+      +- #3 -----------+
        (to #6) <------|  Op. Sem. |      | Simple TC Alg. |
                       +-----------+      +----------------+
                               ^            ^
                                \          /
                                 \        /
          everywhere            +- #1 -----+
       ^    ^    ^    ^         |  Syntax  |
        \   |    |   /          +----------+
         +- #0 -----+
         |   Libs   |
         +----------+

Libraries (#0)

At the bottom level we have general-purpose libraries. This includes the standard libraries that come with Coq (from which we import freely), as well as a few others.

ClassicalReasoningAboutComputation.v: This file contains a convenient axiom base for reasoning about operational semantics. Included are axioms for functional extensionality and propositional extensionality, the axiom of the excluded middle, and the axiom of unique choice. In this development, only the extensionality axioms are used.
Base.v: A small collection of general-purpose tactic definitions.
CompleteInduction.v: A short development proving the complete induction principle for natural numbers.
Maps.v: A simple development of finite maps. Unlike the finite maps in the standard libraries, these maps can hold elements in sort Type.

Program Syntax (#1)

Machine.v The first part of this file defines the abstract syntax of list-machine programs.

Operational Semantics (#2)

Machine.v: The remainder of this file defines the operational semantics of the machine. It also defines the notion of program safety. Finally, a few auxiliary lemmas are proved.

Simple Typechecking Algorithm (#3)

simple_tc.v: This file defines the typechecking algorithm as a set of executable Fixpoint definitions. The typechecker defined here cannot handle the full power of indirect jumps, and thus only typechecks the instruction macro which loads a label and immediately jumps to it. It is almost identical to the algorithm presented by Appel and Leroy [1].

Simple Type System Specification (#4)

simple_tc_safety.v: This file contains both #4 and #5. Box #4 appears first in the file as the Coq module type SIMPLE_TC_SAFETY. It provides the specification of the type system for the simple typechecker.
It includes proof obligations corresponding to the inference rules of the type system and an obligation that the type system is sound. This specification is implemented two different ways (see boxes #6 and #9).

Simple Typechecker Soundness (#5)

simple_tc_safety.v: After the definition of SIMPLE_TC_SAFETY appears the soundness proof for the typechecking algorithm. First we assume an implementation of #4 (by defining a functor in the Coq module system), and using it prove the algorithm sound. This is a straightforward argument by induction that each step of the typechecking algorithm is justified by a rule of the type system.

Syntactic Soundness Proof (#6)

simple_tc_syn.v: This file implements the type system specification defined in #4 via standard proof-theoretic techniques. The typing rules are given by an inductive definition and the safety lemma is proved by a standard progress-and-preservation subject-reduction argument.

Semantic Program Logic (#7)

This is the heart of the semantic proof method. All of the files included in the logic subdirectory as well as the file LMModel.v comprise this portion of the proof.

The development in logic is a completely generic library which defines a shallowly-embedded modal logic using the techniques described by Dockins et. al. [4]. A complete list of the functions, tactics and proof tools exported by this library can be found in the file logic/ModelSpec.v. Unfortunately, this portion of the proof is in dire want of documentation; future releases will contain more extensive comments and discussions of the design decisions.

The file LMModel.v defines the modules necessary to instantiate the model for the list-machine.

Listmachine Hoare Logic (#8)

This portion of the proof consists of the files Listmachine.v and LMHoare.v. Listmachine.v defines operators in the specification logic that are specific to the list-machine setting and proves various properties about them. The file LMHoare.v builds on the model and the operators from Listmachine.v and proves lemmas corresponding to the he rules for a general Hoare logic on list-machine programs.

Semantic Soundness Theorem (#9)

simple_tc_sem.v: Finally we use the Hoare Logic from #8 to prove the rules of the simple typechecker are sound. This mostly involves showing that the type system rules are weaker instances of the rules from the Hoare logic. Finally we prove program safety by appealing to a general result from the logic library.

References

[1] Andrew W. Appel and Xavier Leroy. "A list-machine benchmark for mechanized metatheory." INRIA Research Report RR-5914, May 2006. http://www.inria.fr/rrrt/rr-5914.html.

[2] Andrew W. Appel, Paul-Andre Mellies, Christopher D. Richards, and Jerome Vouillon. "A Very Modal Model of a Modern, Major, General Type System." POPL 2007.

[3] Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. "Oracle Semantics for Concurrent Separation Logic." ESOP 2008.

[4] Robert Dockins, Andrew W. Appel, and Aquinas Hobor. "Multimodal Separation Logic for Reasoning About Operational Semantics." MFPS 2008, to appear.