Struct AtomicUpdate Copy item path

The atomic update (AU) is a ghost object which encapsulates the linearization point of a logically atomic function.

Logical atomicity is a proof technique that allows us to treat a function as if it was atomic, i.e. as if it evaluates in a single atomic step, even though it might perform multiple exec-mode operations internally. The key idea is that a logically atomic function contains a linearization point (LP), that is, a point in the function which updates the state of the program in a single atomic step of computation. We specify the behavior of such a function by describing the state of the program at four distinct points in time, specifically:

• (private pre) at the start of the function,
• (atomic pre) just before the linearization point,
• (atomic post) just after the linearization point,
• (private post) at the end of the function.

                       linearization point
                                🠗
├──────────────────────────────┤●├─────────────────────────┤
 private                 atomic   atomic            private
 pre                        pre   post                 post

The AtomicUpdate ghost object is the central abstraction for our implementation if logical atomicity, as it encapsulates the behavior of the function at the linearization point. The atomic update is declared by the atomic specification, it is constructed by the atomic function call (i.e. the “client”), and it is opened/destructed at the linearization point of the logically atomic function (i.e. the “library”).