In this report, I will explain how I benefitted from Prof. Ursula Martin's NETCA grant and what I achieved as a result.

During this NETCA-supported visit to Queen Mary, I obtained two results. First, I developed a new method for proving data refinement of low-level pointer programs, jointly with Ivana Mijajlovic, who is a PhD student in Queen Mary, University of London. Data refinement is a process in which the concrete representation of some abstract module is formally derived. Surprisingly, none of the existing methods for data refinement are sound in the presence of low-level pointer operations, such as memory allocation/deallocation and pointer arithmetic. The main reason is that the low-level pointer operations allow two new methods for obtaining the information about the implementation details of the module: a client of a module can directly access the internal cells of the module by dereferencing pointers, or it can find out which cells are internally used by the module, using memory allocation and pointer comparison. The unsoundness of the existing methods comes from the failure of handling these methods. During my visit, Mijajlovic and I developed a new data-refinement method, which we call power simulation, and proved that power simulation is sound even with low-level pointer operations. We also demonstrated that the power simulation is strong enough to validate interesting low-level optimizations used in the systems code, such as the optimization of a doubly-linked list by an xor list in a queue module. A paper about power simulation was submitted to the third Asian symposium on programming languages and systems (APLAS 2005).

Second, with Prof. Peter O'Hearn in Queen Mary and Dr. Cristiano Calcagno in Imperial College, I found a simpler soundness proof of concurrent separation logic. Concurrent separation logic is an extension of Hoare logic for concurrent pointer programs, and it contains elegant proof rules for verifying properties about concurrency. An available soundness proof of concurrent separation logic is Brookes's. Although this soundness proof contains many interesting ideas, such as action traces and invariant-based execution of a trace, it is big and complex, so that the proof does not provide an immediate insight about how much the logic can be generalized without losing soundness. During the NETCA-supported visit, with O'Hearn and Calcagno, I found an alternative simpler soundness proof of the logic. The obtained proof borrows the ideas from Brookes's original soundness proof, but it is based on Plotkin's structural operational semantics, so as to avoid the complications from traces in Brookes's soundness proof. Currently, O'Hearn, Calcagno and I are investigating how much the new soundness proof can be generalized, in order to obtain a more general version of concurrent separation logic.