Inferring Synchronization under Limited Observability
Martin Vechev, Eran Yahav, Greta Yorsh
In Proc. Tools and Algorithms for the Construction and Analysis of Systems, 2009
This paper addresses the problem of automatically inferring
synchronization for concurrent programs.
Given a program and a specification, we infer synchronization
that avoids all interleavings violating the specification, but
permits as many valid interleavings as possible.
We let the user specify an upper bound on the cost of synchronization,
which may limit the observability - what
observations on program state can be made by the synchronization code.
We present an algorithm that infers, under certain conditions, the
maximally permissive synchronization for a given cost.
We implemented a prototype of our approach and applied it to
infer synchronization in a number of small programs.
Click here to access the technical report: