Verification Of Separate Compilation For Concurrent Programs

Many practical computer programs are concurrent programs consisting of multi-ple program modules.Separate compilation is important for such programs,it compiles program modules independently then link them into executable program.Correct com-pilation needs to guarantee that the target modules can work together and preserve the semantics of the source program as a whole.It requires not only that individual mod-ules be compiled correctly,but also that the expected interactions between modules be preserved at the target.This dissertation studies the formulation and verification technique of separate compilation for concurrent programs,and makes the following contributions.First,it propose a verification framework that builds certified separation compi-lation for concurrent programs from certified sequential compilation.The framework employs a novel compositional footprint-preserving simulation as the correctness crite-ria of compilation for sequential modules.It considers module interaction between both external function calls and synchronization points,thus is compositional with respect to both module linking and non-preemptive concurrency.It also requires the footprint(the set of memory locations accessed during the execution)of the source and target modules to be related,and reduces the proof of the preservation of DRF,a whole pro-gram property,to the proof of local footprint preservation.In addition,the framework works with an abstract program language.It abstracted away language details such as specific synchronization constructs:and concrete primitives that access memory.As a result,the lemmas in the framework are re-usable when instantiating to real languages.Second,it extends the framework above to support targeting x86-TSO machine,and linking with efficient concurrent x86-TSO object implementations which may con-tain races,e.g.spin-locks in Linux.In the framework extension,it presents a correct-ness formulation for x86-TSO object implementations,and guarantees its soundness by proving a strengthened DRF-guarantee theorem for the x86-TSO model.Finally,with the framework it develops CASCompCert,which extends the prac-tical CompCert C compiler for certified separate compilation for race-free concurrent programs.As an application of the framework extension,it proves the correctness of an efficient x86-TSO spin-lock implementation,which could be linked with DRF pro-grams compiled by CASCompCert for synchronization.The proofs are all mechanized in the Coq proof assistant.