A Formal Approach To Build Safe Threading Machanisms

As the application of concurrenct systems is widely accepted, their safety is growing more and more important. Most of former research focused on how to guarantee the the safety of concurrent programs with the safety of the implementation for concurrent mechanisms trusted. Research on the safety of the concurrent mechanisms themselves was either based on an over-abstracted model to make the reasoning impractical, or rather complex and need very tedious proof. This is why we still use the practical dynamic testing as the major way to ensure the safety of operating systems or thread libraries.We are eager to see that the formal reasoning can be used more in real-world concurrent systems, and this paper is a solid step towards our goal. In this paper, we propose a verification framework for low-level code reasoning, and use it to prove the safety of a thread library. The library is runnable on real physical machines. And the complexity of proof on our framework is much less than that of other similar framworks. More importantly, we prove not just the safety of the library itself, but also the safety of the interaction between the library and its clients. To make our framework more applicable on more complicated code, we also do much work on simplifying the program specification and reducing the cost of proof.All formal work in this paper is implemented in the Coq proof assistant. It means that the soundness proof of our framework and the safety proof of the library is machine checkable. Their safety also does not rely on any compilers, making our thread library a proof-carrying code package, which can be directly used in the systems where the safety property is very critical.