Please use this identifier to cite or link to this item:
|Title:||Contextual trace refinement for concurrent objects: Safety and progress|
|Citation:||18th International Conference on Formal Engineering Methods, 2016|
|Abstract:||Correctness of concurrent objects is defined in terms of safety properties such as linearizability, sequential consistency, and quiescent consistency, and progress properties such as wait-, lock-, and obstruction-freedom. These properties, however, only refer to the behaviour of the object in isolation, which does not tell us what guarantees these correctness conditions on concurrent objects provide to their client programs. This paper investigates the links between safety and progress properties of concurrent objects and a form of trace refinement for client programs, called contextual trace refinement. In particular, we show that linearizability together with a minimal notion of progress are sufficient properties of concurrent objects to ensure contextual trace refinement, but sequential consistency and quiescent consistency are both too weak. Our reasoning is carried out in the action systems framework with procedure calls, which we extend to cope with non-atomic operations.|
|Appears in Collections:||Dept of Computer Science Research Papers|
Items in BURA are protected by copyright, with all rights reserved, unless otherwise indicated.