Re: Semantics Tools

eifrig@beanworld.cs.jhu.edu (Jonathan Eifrig) writes:
> Curiously, I was wondering something related: How many people are
>using formal semantic methods to either (1) generate a compiler or (2)
>prove a compiler correct in "real life?" My gut feeling was "not many,"
>but then I started thinking about some of the transformational and
>continuations-based compilation approaches that have been published in
>the last few years, and started wondering.


At Oxford, we are studying the verification of compiling specifications,
and their rapid prototyping using logic programming. The compiler is
specified as a set of theorems (to be proved correct with respect to the
refinement ordering of the language) which turn out to be in the form of
Horn clauses in general. A novel aspect of the approach (due to Prof
C.A.R. Hoare) is that the target machine is defined in terms of an
interpreter written in the high-level language to be copiled. This allows
the proofs to be undertaken largely algebraically using laws about the
programming laguage. We have used variants of Occam and the transputer as
own paradigm, and are currently investigating compilation to a "normal
form" that could allow "code generation" down to either a traditional
instruction set, or a netlist of hardware components for implementation on
a Field Programmable Gate Array, or a combination of both. We have also
used OBJ3 as a term rewriting system, that also allows a rapid prototype
implementation of a compiler, rewriting the source program to a normal
form that is close to object code and are considering code optimisation
which is often lacking in formal approaches. We have even considered how a
decompiler may be produced almost directly from the compiling
specification since the logic program specifies a relation that is
essentially reversible (although termination problems, etc., must be
considered). Constraint Logic Programming (CLP) may well help to solve
some of the problems of using logic programming by allowing a more
declarative approach to the implementation of the constraint predicates
involved in the compiling theorems.


Much of the work (and the inspiration behind its inception) is due to the
European collaborative ESPRIT Basic Research ProCoS project ("Provably
Correct Systems"). This project is investigating verification techniques
for the entire development process from requirements through to
specification, program, object code and ultimately the hardware itself.
Another group on the project at Kiel University (in Germany) are
investigating the verification of a more realistic compiler, including the
bootstrapping a verified compiler, using an operation semantics approach,
but this is a longer term problem.


Below are some references for those interested in following up the various
aspects of this work.


An overview of the verification and rapid prototyping approach:


Bowen JP, He Jifeng, Pandya PK.
An approach to verifiable compiling specification and prototyping.
In: Deransart P, Ma\l{}uszy\'nski J (eds)
Programming Language Implementation and Logic Programming.
International Workshop PLILP 90.
Springer-Verlag, 1990, pp 45--59
(Lecture notes in computer science no. 456)


A comparive study of using theorem provers (including OBJ3):


Augusto Sampaio.
A comparative study of theorem provers:
  proving correctness of compiling specifications.
Programming Research Group Technical Report TR-20-90, 1990, 50 p.


A presentation of the underlying verification approach:


Hoare CAR.
Refinement algebra proves correctness of compiling specifications.
In: Morgan CC, Woodcock JCP (eds)
3rd Refinement Workshop.
Springer-Verlag, 1991, pp 33--48
(Workshops in computing)
(Also issued as a Programming Research Group Technical Report PRG-TR-6-90)


An overview of the work on the ProCoS project:


Hoare CAR, He Jifeng, Bowen JP, Pandya PK.
An algebraic approach to verifiable
compiling specification and prototyping
of the ProCoS level 0 programming language.
In: Directorate-General of the
Commission of the European Communities (eds)
ESPRIT '90 Conference Proceedings, Brussels.
Kluwer Academic Publishers B.V., 1990, pp 804--818


A more detailed presentation of the ProCoS work:


He Jifeng, Olderog ER (eds).
Interfaces between Languages for Concurrent Systems. Vol 2,
ESPRIT BRA 3104 Provably Correct Systems
  ProCoS Draft Final Deliverable,
October 1991 (To be issued as a Technical Report, DTH, Denmark)


Another approach to compiler verification (using operational semantics):


von Karger, B. (ed).
Compiler development. Vol 3,
ESPRIT BRA 3104, Provably Correct Systems
  ProCoS Draft Final Deliverable,
October 1991 (To be issued as a Technical Report, DTH, Denmark)


An overview of compilation directly into hardware:


Page I, Luk W.
Compiling Occam into field-programmable gate arrays.
in Moore W, Luk W (eds),
FPGAs,
Oxford Workshop on Field Programmable Logic and Applications.
Abingdon EE\&CS Books, 15 Harcourt Way, Abingdon OX14 1NV, UK,
1991


A detailed account of the logic programming approach to decompilation:


Jonathan Bowen.
>From Programs to Object Code and back again using Logic Programming.
ESPRIT II REDO Project Document 2487-TN-PRG-1044, 1991.


An example of a real-time programming language and a compiler:


He Jifeng and Jonathan Bowen.
Time Interval Semantics and Implementation of a Real-Time
  Programming Language.
In Proc. Fourth Euromicro Workshop on Real-Time Systems,
IEEE Computer Society Press, pp~110--115, June 1992.


Information on the rapid prototyping approach using logic programming:


Jonathan Bowen.
>From Programs to Object Code using Logic and Logic Programming.
In: Robert Giegerich and Susan L.\ Graham (eds),
Code Generation -- Concepts, Tools, Techniques,
Proceedings of the International Workshop on Code
Generation, Dagstuhl, Germany, 20--24 May 1991.
Springer-Verlag, Workshops in Computing, August 1992.


An overview of two approaches to decompilation:


Bowen JP, Breuer PT.
Decompilation.
In: van Zuylen H (ed)
The REDO Handbook:
A Compendium of Reverse Engineering for Software Maintenance,
chapter 9,
Wiley, 1992 (To appear)


A more detailed account of decompilation using functional/logic approaches:


Peter Breuer and Jonathan Bowen.
Decompilation: the Enumeration of Types and Grammars.
Programming Research Group Technical Report TR-11-92, 1992.
(A shortened version is to be presented at the Workshop on Static
Analysis 92, Bordeaux, France, 23--25 September 1992.)


Hardware compilation:


He Jifeng, Ian Page and Jonathan Bowen.
{\em Normal Form Approach to FPGA Implementation of occam},
ProCoS project document [OU HJF 9/2], January 1992.
(Draft, available on request)


An example of compiler optimisation:


He Jifeng and Jonathan Bowen.
Specification, Verification and Prototyping of an Optimized Compiler.
1992. (Draft, available on request)




Programming Research Group Technical Reports and REDO project documents
are available from our librarian on <library@comlab.ox.ac.uk>.
--
Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk>
Oxford University Computing Laboratory.
--

Return to the comp.compilers page.
Search the comp.compilers archives again.