The automatic detection of token structures and invariants using SAT checking
Many distributed systems rely on token structures for their correct operation. Often, these structures make sure that a fixed number of tokens exists at all times, or perhaps that tokens cannot be completely eliminated, to prevent systems from reaching undesired states. In this paper we show how a S...
| Príomhchruthaitheoirí: | , , |
|---|---|
| Formáid: | Conference item |
| Foilsithe / Cruthaithe: |
Springer, Berlin, Heidelberg
2017
|
| Achoimre: | Many distributed systems rely on token structures for their correct operation. Often, these structures make sure that a fixed number of tokens exists at all times, or perhaps that tokens cannot be completely eliminated, to prevent systems from reaching undesired states. In this paper we show how a SAT checker can be used to automatically detect token and similar invariants in distributed systems, and how these invariants can improve the precision of a deadlock-checking framework that is based on local analysis. We demonstrate by a series of practical experiments that this new framework is as efficient as similar incomplete techniques for deadlock-freedom analysis, while handling a different class of systems. |
|---|