Parameterized Verification of Asynchronous Shared-Memory Systems

March 24, 2015

Pierre Ganty


Parameterized Verification of Asynchronous Shared-Memory Systems

Time:   10:45am
Location:   Lecture hall 1, level B

We study systems consisting of a leader process and arbitrarily many anonymous and identical contributors. Processes communicate through a shared, bounded-value register. While each operation on the register is atomic, there is no synchronization primitive to execute a sequence of operations atomically. We analyze the complexity of the safety verification problem. We consider the cases where leader and contributors are in turn modeled by finite-state machines, pushdown machines, and Turing machines. Our proofs use a mix of combinatorial properties of the model and some language-theoretic constructions of independent interest. We will also present preliminary results about the liveness verification problem.