The Piton Project

Piton is a simple assembly-level programming language. A sample Piton program is:


Subroutine big-add(a b n)
       push-constant f     ; push false on the stack
       push-local a        ; push the value of variable a
loop   fetch               ; pop an address, fetch and push contents
       push-local b        ; push the value of b
       fetch               ; pop an address, fetch and push contents
       add-nat-with-carry  ; add the 2 topmost elements
       ...

Piton provides execute-only programs, recursive subroutine call and return, stack-based parameter passing, local variables, global variables and arrays, a user-visible stack for intermediate results, and seven type-safe abstract data types including integers, data addresses, program addresses and subroutine names. The semantics of Piton is given by an Nqthm function.

Piton has been implemented on the FM9001, a 32-bit general purpose microprocessor with 16 general purpose 32-bit wide registers, four 1-bit condition code registers and up to 2^32 words of memory. Using Nqthm, Warren Hunt and Bishop Brock proved that FM9001 was correctly implemented by an NDL netlist. That netlist was then fabricated by LSI Logic, Inc.

The implementation of Piton on the FM9001 is via an assembler/linker that maps a system of Piton programs and data declarations into a binary image for the FM9001.


00001111111000001000100000000001
00001111111000000000010000000010
00001111111000001000100000110011
...

The assembler/linker is written as an Nqthm function. Using Nqthm, I proved (with help from Matt Kaufmann), that Piton is correctly implemented on the FM9001. In particular, I proved

The Piton Correctness Theorem: If

p is a proper Piton state with wordsize 32,
load-addr is a natural number,
p is loadable starting at location load-addr, and
no error occurs when Piton runs n steps from p,
then the data produced by the n-step run above can be alternatively produced by

assembling and linking p into a binary image at load-addr,
running FM9001 a certain number of steps (given by a constructively defined function of p and n), and
disassemblying the resulting registers and memory according to a function of certain tables produced by the assembler/linker.

Piton provides a convenient abstract machine upon which one can build compilers for higher level languages. Such compilers have been built and verified (e.g., by Bill Young and Art Flatau). In addition, applications programs have been coded directly in Piton and verified (e.g., by Matt Wilding).

Piton is a part of the CLI Stack, a sequence of languages and/or computing machines, each implemented atop the previous one,

and involves work by Bill Bevier, Bishop Brock, Warren Hunt, Matt Kaufmann, and Bill Young, in addition to me.

For details of the Piton Project, see

Piton: A Mechanically Verified Assembly-Level Language, J Strother Moore, Automated Reasoning Series, Kluwer Academic Publishers, 1996.

[Best Ideas] [Publications] [Research] [Home]