Disjoint Fractional Permissions in Verification: Applications, Systems and Theory
COM1 Level 3
MR1, COM1-03-19
Abstract:
Fractional permissions enable sophisticated management and reasoning over resource ownership in Concurrent Separation Logic (CSL). One common model of permissions uses rational numbers between 0 and 1 as permissions and addition for splitting/joining permissions. While the rational model is simple, it poses a technical challenge to the core property of CSL that allows compositional reasoning. As a result, there has been substantial work in proposing better models for fractional permissions in the last twenty years.
In this thesis, we propose a disjoint fractional permission model to fix the shortcomings of rational model. Our main contribution is a comprehensive study of the disjoint permissions via three different aspects: applications, systems, and theory.
In particular, we develop an expressive rewriting proof system with disjoint permissions for CSL. Our framework can handle sophisticated verification tasks such as induction and bi-abduction reasoning. Our proof rules are prototyped into the tool ShareInfer and yield a reasonable performance. We also devise several complete decision procedures to solve different types of disjoint permissions constraint extracted from verification tool HIP/SLEEK. Our procedures are certified in the theorem prover Coq and thus are guaranteed bug-free. For theory aspect, we obtain various decidability and complexity results over the first-order theory of disjoint permission model using connections to automatic structures, word equations and Boolean Algebras.