Shared boxes: rely-guarantee reasoning in VeriFast

摘要

VeriFast is a verifier for single-threaded and multithreaded C and Java programs. It takes a C or Java program annotated with preconditions and postconditions in a separation logic notation, and verifies statically that these preconditions and postconditions hold, using symbolic execution. In plain separation logic, a thread either has full ownership of a memory location and knows the value at the location, or it has no ownership and no knowledge of the value of the location. Existing work proposes a marriage of rely-guarantee reasoning and separation logic to address this. In this document, we describe the shared boxes mechanism, which marries separation logic and rely-guarantee reasoning in VeriFast. We introduce and motivate the shared boxes mechanism using a minimalistic example and a realistic example. The minimalistic example is a counter program where one thread continuously increments a counter and other threads check that the counter does not decrease. For the realistic example, we verify functional correctness of the Michael-Scott queue, a lock-free concurrent data structure. We define the syntax and semantics of a simple C-like programming language, and we define a separation logic with shared boxes and prove its soundness. We discuss the implementation in VeriFast and the examples we verified using our VeriFast implementation.