master-degree-notes/Concurrent Systems/notes/6 - Atomicity.md

We have a set of n sequential processes p_{1},...,p_n , that access m concurrent objects X_1,...,X_m by invoking operations on the form Xi.op(args)(ret).

When invoked by p_j, the invocation Xi.op(args)(ret) is modeled by two events: inv[Xi.op(args) by pj] and res[Xi.op(ret) to pj].

A history (or trace) is a pair \hat{H}=(H, <_{H}) where H is a set of events and <_{H} is a total order on them.