home *** CD-ROM | disk | FTP | other *** search
/ NetNews Usenet Archive 1992 #19 / NN_1992_19.iso / spool / comp / compiler / 1456 < prev    next >
Encoding:
Internet Message Format  |  1992-08-29  |  7.6 KB
  1. Path: sparky!uunet!gatech!rutgers!faatcrl!iecc!compilers-sender
  2. From: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen)
  3. Newsgroups: comp.compilers
  4. Subject: Re: Semantics Tools
  5. Summary: Compiler verification and prototyping
  6. Keywords: theory, bibliography
  7. Message-ID: <92-08-158@comp.compilers>
  8. Date: 26 Aug 92 13:32:48 GMT
  9. References: <92-08-153@comp.compilers>
  10. Sender: compilers-sender@iecc.cambridge.ma.us
  11. Reply-To: Jonathan.Bowen@prg.oxford.ac.uk (Jonathan Bowen)
  12. Organization: Programming Research Group, Oxford University, UK
  13. Lines: 174
  14. Approved: compilers@iecc.cambridge.ma.us
  15.  
  16. eifrig@beanworld.cs.jhu.edu (Jonathan Eifrig) writes:
  17. >    Curiously, I was wondering something related: How many people are
  18. >using formal semantic methods to either (1) generate a compiler or (2)
  19. >prove a compiler correct in "real life?"  My gut feeling was "not many,"
  20. >but then I started thinking about some of the transformational and
  21. >continuations-based compilation approaches that have been published in
  22. >the last few years, and started wondering.
  23.  
  24. At Oxford, we are studying the verification of compiling specifications,
  25. and their rapid prototyping using logic programming.  The compiler is
  26. specified as a set of theorems (to be proved correct with respect to the
  27. refinement ordering of the language) which turn out to be in the form of
  28. Horn clauses in general. A novel aspect of the approach (due to Prof
  29. C.A.R. Hoare) is that the target machine is defined in terms of an
  30. interpreter written in the high-level language to be copiled. This allows
  31. the proofs to be undertaken largely algebraically using laws about the
  32. programming laguage. We have used variants of Occam and the transputer as
  33. own paradigm, and are currently investigating compilation to a "normal
  34. form" that could allow "code generation" down to either a traditional
  35. instruction set, or a netlist of hardware components for implementation on
  36. a Field Programmable Gate Array, or a combination of both. We have also
  37. used OBJ3 as a term rewriting system, that also allows a rapid prototype
  38. implementation of a compiler, rewriting the source program to a normal
  39. form that is close to object code and are considering code optimisation
  40. which is often lacking in formal approaches. We have even considered how a
  41. decompiler may be produced almost directly from the compiling
  42. specification since the logic program specifies a relation that is
  43. essentially reversible (although termination problems, etc., must be
  44. considered). Constraint Logic Programming (CLP) may well help to solve
  45. some of the problems of using logic programming by allowing a more
  46. declarative approach to the implementation of the constraint predicates
  47. involved in the compiling theorems.
  48.  
  49. Much of the work (and the inspiration behind its inception) is due to the
  50. European collaborative ESPRIT Basic Research ProCoS project ("Provably
  51. Correct Systems"). This project is investigating verification techniques
  52. for the entire development process from requirements through to
  53. specification, program, object code and ultimately the hardware itself.
  54. Another group on the project at Kiel University (in Germany) are
  55. investigating the verification of a more realistic compiler, including the
  56. bootstrapping a verified compiler, using an operation semantics approach,
  57. but this is a longer term problem.
  58.  
  59. Below are some references for those interested in following up the various
  60. aspects of this work.
  61.  
  62. An overview of the verification and rapid prototyping approach:
  63.  
  64. Bowen JP, He Jifeng, Pandya PK.
  65. An approach to verifiable compiling specification and prototyping.
  66. In: Deransart P, Ma\l{}uszy\'nski J (eds)
  67. Programming Language Implementation and Logic Programming.
  68. International Workshop PLILP 90.
  69. Springer-Verlag, 1990, pp 45--59
  70. (Lecture notes in computer science no. 456)
  71.  
  72. A comparive study of using theorem provers (including OBJ3):
  73.  
  74. Augusto Sampaio.
  75. A comparative study of theorem provers:
  76.  proving correctness of compiling specifications.
  77. Programming Research Group Technical Report TR-20-90, 1990, 50 p.
  78.  
  79. A presentation of the underlying verification approach:
  80.  
  81. Hoare CAR.
  82. Refinement algebra proves correctness of compiling specifications.
  83. In: Morgan CC, Woodcock JCP (eds)
  84. 3rd Refinement Workshop.
  85. Springer-Verlag, 1991, pp 33--48
  86. (Workshops in computing)
  87. (Also issued as a Programming Research Group Technical Report PRG-TR-6-90)
  88.  
  89. An overview of the work on the ProCoS project:
  90.  
  91. Hoare CAR, He Jifeng, Bowen JP, Pandya PK.
  92. An algebraic approach to verifiable
  93. compiling specification and prototyping
  94. of the ProCoS level 0 programming language.
  95. In: Directorate-General of the
  96. Commission of the European Communities (eds)
  97. ESPRIT '90 Conference Proceedings, Brussels.
  98. Kluwer Academic Publishers B.V., 1990, pp 804--818
  99.  
  100. A more detailed presentation of the ProCoS work:
  101.  
  102. He Jifeng, Olderog ER (eds).
  103. Interfaces between Languages for Concurrent Systems. Vol 2,
  104. ESPRIT BRA 3104 Provably Correct Systems
  105.  ProCoS Draft Final Deliverable,
  106. October 1991 (To be issued as a Technical Report, DTH, Denmark)
  107.  
  108. Another approach to compiler verification (using operational semantics):
  109.  
  110. von Karger, B. (ed).
  111. Compiler development. Vol 3,
  112. ESPRIT BRA 3104, Provably Correct Systems
  113.  ProCoS Draft Final Deliverable,
  114. October 1991 (To be issued as a Technical Report, DTH, Denmark)
  115.  
  116. An overview of compilation directly into hardware:
  117.  
  118. Page I, Luk W.
  119. Compiling Occam into field-programmable gate arrays.
  120. in Moore W, Luk W (eds),
  121. FPGAs,
  122. Oxford Workshop on Field Programmable Logic and Applications.
  123. Abingdon EE\&CS Books, 15 Harcourt Way, Abingdon OX14 1NV, UK,
  124. 1991
  125.  
  126. A detailed account of the logic programming approach to decompilation:
  127.  
  128. Jonathan Bowen.
  129. >From Programs to Object Code and back again using Logic Programming.
  130. ESPRIT II REDO Project Document 2487-TN-PRG-1044, 1991.
  131.  
  132. An example of a real-time programming language and a compiler:
  133.  
  134. He Jifeng and Jonathan Bowen.
  135. Time Interval Semantics and Implementation of a Real-Time
  136.  Programming Language.
  137. In Proc. Fourth Euromicro Workshop on Real-Time Systems,
  138. IEEE Computer Society Press, pp~110--115, June 1992.
  139.  
  140. Information on the rapid prototyping approach using logic programming:
  141.  
  142. Jonathan Bowen.
  143. >From Programs to Object Code using Logic and Logic Programming.
  144. In: Robert Giegerich and Susan L.\ Graham (eds),
  145. Code Generation -- Concepts, Tools, Techniques,
  146. Proceedings of the International Workshop on Code
  147. Generation, Dagstuhl, Germany, 20--24 May 1991.
  148. Springer-Verlag, Workshops in Computing, August 1992.
  149.  
  150. An overview of two approaches to decompilation:
  151.  
  152. Bowen JP, Breuer PT.
  153. Decompilation.
  154. In: van Zuylen H (ed)
  155. The REDO Handbook:
  156. A Compendium of Reverse Engineering for Software Maintenance,
  157. chapter 9,
  158. Wiley, 1992 (To appear)
  159.  
  160. A more detailed account of decompilation using functional/logic approaches:
  161.  
  162. Peter Breuer and Jonathan Bowen.
  163. Decompilation: the Enumeration of Types and Grammars.
  164. Programming Research Group Technical Report TR-11-92, 1992.
  165. (A shortened version is to be presented at the Workshop on Static
  166. Analysis 92, Bordeaux, France, 23--25 September 1992.)
  167.  
  168. Hardware compilation:
  169.  
  170. He Jifeng, Ian Page and Jonathan Bowen.
  171. {\em Normal Form Approach to FPGA Implementation of occam},
  172. ProCoS project document [OU HJF 9/2], January 1992.
  173. (Draft, available on request)
  174.  
  175. An example of compiler optimisation:
  176.  
  177. He Jifeng and Jonathan Bowen.
  178. Specification, Verification and Prototyping of an Optimized Compiler.
  179. 1992.  (Draft, available on request)
  180.  
  181.  
  182. Programming Research Group Technical Reports and REDO project documents
  183. are available from our librarian on <library@comlab.ox.ac.uk>.
  184. --
  185. Jonathan Bowen, <Jonathan.Bowen@comlab.ox.ac.uk>
  186. Oxford University Computing Laboratory.
  187. -- 
  188. Send compilers articles to compilers@iecc.cambridge.ma.us or
  189. {ima | spdcc | world}!iecc!compilers.  Meta-mail to compilers-request.
  190.