Researcher Joakim Öhman, supervised by Professor Aleks Nanevski, presented his thesis: “Compositional Reasoning of Concurrency with the Visibility Method” on April 15 at the IMDEA Software Institute, accompanied by colleagues and family members.
To further improve efficiency of programs in the post Dennard scaling age, development of concurrent programs is essential. Concurrent programs consist of multiple procedures running in parallel, so-called threads, which at some point need to synchronize to produce a unified result. The choice of synchronization largely determines how well the program can run concurrently, thus influencing its efficiency.
The thesis unveils a modular approach to proving the linearizability of concurrent snapshot algorithms, significantly enhancing our understanding and formalizing previously informal concepts. Linearizability effectively ensures that a concurrent algorithm behaves correctly, such that one can replace a sequential algorithm with a concurrent one seamlessly, without any deviations in operation. Without a proof of linearizability, an algorithm may behave unexpectedly and exhibit bugs, particularly considering the inherent unpredictability of concurrency.
Joakim presented modular proofs for three snapshot algorithms developed by Jayanti and one by Afek et al., all achieved through the innovative use of visibility reasoning, originally introduced by Henzinger et al. In a bid to streamline the proof process, the linearizability proofs were disassembled into individual proof modules. Notably, a substantial number of these modules were shared across the three algorithms, emphasizing efficiency by developing once and reusing multiple times to curtail proof complexity.
The crux of this advancement lies in the module interfaces, which are composed of relations and axioms. One module, in particular, encapsulates the pivotal concept of “forwarding” that forms the backbone of Jayanti’s design. This work has successfully demonstrated that a formalism grounded in visibility reasoning can adeptly capture these intricate principles, which were previously only articulated informally by Jayanti in English.
Diverging from the conventional simulation approaches to linearizability, the visibility approach zeroes in on pinpointing the essentials required to establish linearizability. However, determining these essentials for data structures with arbitrary partial order of operations can pose formidable challenges.
In a strategic blend of methodologies, this research leveraged ideas from both approaches. By assuming a total order between specific operations, the task of identifying the essentials for linearizability was streamlined. This amalgamation proved crucial, as developing a coherent snapshot structure specification without presupposing a total order among writers of the same cell proved to be an arduous endeavor.
This innovative research not only refines our understanding of snapshot algorithms but also showcases the potential of visibility reasoning as a robust tool for formalizing complex concurrent programming concepts.
