Modeling concurrent algorithms
You have mentioned the temporal ordering of events, then you may have known about temporal logic [1] such as LTL [2] and CTL [3]. Temporal logic allows you to reason about time and thus temporal ordering of events. For instance (from [1]), one may wish to say that whenever a request is made, access to a resource is eventually granted, but it is never granted to two requestors simultaneously. 

The greatest advantage of using LTL or CTL to express the properties of the system is that you can automatically verify them. This process is known as model checking [4]. 

There are quite a few of model checkers [5]. For instance, in SPIN, systems to be verified are described in Promela (Process Meta Language), which allows one to specify "atomic blocks" (Is this your intention of What transactions need to be atomic?)?

As for the producer/consumer problem, it has been extensively studied in the context of model checking. This lecture note uses it as an example for SPIN (you can easily find other resources). In addition, [6] verifies an edition written in SystemC, and [7] verifies it using TLA+.



[1] temporal logic (wiki)

[2] LTL (wiki)

[3] CTL (wiki)

[4] model checking (wiki)

[5] model checkers (wiki)

[6] Verifying SystemC: a Software Model Checking Approach

[7] An Example of Debugging Java with a Model Checker (web page)