Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
Inferring Synchronization under Limited Observability
verfasst von : Martin Vechev, Eran Yahav, Greta Yorsh
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.