Yale internship

March to August 2010

With Zhong Shao.

Place

Computer Science department of Yale University (New Haven, USA)

Final report

Available as a PDF.

Done

• part of the OS class attempted
• Coq formalization of a part of Local Action and Abstract Separation Logic
• Incrementation operation added to CompCert
• beginning of a sample PCC and compiler implementation in Coq
• proof of safety of an optimistic queue : report
• project of Coq formalization of historical logic for concurrent programs, with Yannis Kouskoulas

TODO

• Proof on mixed C and assembly :
  • try to add in-lined assembly code extension to a toy language
  • read OCAP framework
  • read Syntactic Proofs of Compositional Compiler Correctness
  • use CompCert theorem to translate Hoare assertions on C to assembly PCC

Timeline

Week 19

• Tuesday : logical axioms used to simplify equivalence classes of assertions and trace equality
• Wednesday : code reorganisation for transition semantics, proof of ENV rule

Week 18

• Monday, Tuesday : still working on the Coq historical logic formalization
• Wednesday : now traces cannot be empty

Week 17

• Monday : discussions about what to do next for historical logic and for a Coq implementation with Yanni
• Tuesday : reading about prophecy variables and the QED system
• Wednesday : coming back to the Coq code with a report on it
• Tuesday, Friday : cleaning of the Coq code, discussions with Yanni for an implementation design choice

Week 16

• Monday : beginning of a precise proof added to the report
• Tuesday, Wednesday : precise proof of "enqueue"
• Thursday : beginning of a precise proof for "dequeue", properties to ensure the guarantee
• Friday : end of the queue proof

Week 15

• Monday : proof of MCAS abandoned (historical logic not important), work on optimistic queue instead : report
• Tuesday : formalization of queue safety property
• Wednesday : key properties + sketch of the proof
• Thursday : discussions on the proof + potential dereferencing bug found
• Friday : in the train ; partially read articles : Mozes - Shavit queues, queues with GC verification, the Repeat Offender Problem

Week 14

• proof of the simple optimistic incrementation example
• thinking about logical variables formalization
• beginning of proof of MCAS

Week 13

• Monday : Coq : soundness formalization updated to the new report version
• Tuesday : Coq : code refractored into multiple files
• Wednesday : sick
• Thursday : work on Fu's stack proof
• Friday : work on Fu's stack proof + looking for other algorithms

Week 12

• Monday : Coq
• Tuesday : Coq
• Wednesday : Coq : soundness proof for 2 sequential rules
• Thursday : Coq : formalization of last cases for sequential rules, beginning of RG rules
• Friday : Coq : soundness theorems formalization

Week 11

• Monday : application of RGSep in Victor's PhD read
• Tuesday : Ming Fu's logic formalization started
• Wednesday : Coq
• Thursday : Coq
• Friday : Coq

Week 10

• Syntactic Proofs of Compositional Compiler Correctness read
• beginning of a sample PCC and compiler implementation in Coq
• beginning of OCAP framework read

Week 9

• unsuccessful tests on a toy language with in-lined C code : Coq source
• NEPLS seminar

Week 8

• Incrementation operation added to CompCert
• Look at the external function calls formalisation

Week 7

• Coq formalization of a part of Local Action and Abstract Separation Logic
• Local Action and Abstract Separation Logic read (until section 5)
• Singularity: Rethinking the Software Stack read
• beginning of a report

Week 6

• look CompCert source code
• learn basis about the PowerPC assembly
• Coq, CompCert, cross compiler chain, PowerPC emulator installed

Week 5

• Formal verification of a C compiler front-end paper read
• Formal verification of a realistic compiler paper read
• OS class 18 (Microkernels and capabilities) attempted
• A formally verified compiler back-end paper looked

Week 4

• paper Formal Modeling and Analysis of a Flash File System in Alloy read
• paper Modelling and Proof of a Tree-Structured File System in Event-B and Rodin read
• looking for interesting papers about file system formalization
• first OS class attempted (about file systems)

Week 3

• trying to catch the OS class during Spring Break

Week 2

• trying to catch the OS class during Spring Break
• papers about logic read

Week 1

• administrative stuffs