Modeling concurrent algorithms

I'm working on a class library (C++) that can be thought of as a producer/consumer queue of producer/consumer queues. There are many queues of data, and the goal is to assign worker threads to process these queues, as needed, using coroutines. At any rate, the details aren't necessarily important to the question, but I'm struggling to wrap my head fully around the synchronization requirements.

I've started with a list of basic operations (like adding an element to the top level queue), along with some preconditions, postconditions, and what I'm calling "exclusions" which are things that are not supposed to happen during the operation. It seems to only scratch the surface though.

Finally, my question: Is there a way to model algorithms (either notation or diagram) that helps to tease out temporal ordering requirements? What needs to be locked when? What transactions need to be atomic? What order can reads/writes be carried out in?

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)

StackExchange Computer Science Q#38015, answer score: 3