Atomic Blocks for Concurrency?

[DavePearce]

Given the introduction of lifetimes (#642) and some potential solutions for ownership (#646), I'm starting to think again about concurrency. In particular, the question is: what primitive could we add that would support concurrency?

The chosen primitive should allow one to write locks, mutexes, shared channels, etc. One options would be to support atomic blocks or atomic instructions. An interesting observation is the support for this provided by LLVM and C++:

http://llvm.org/docs/Atomics.html
http://en.cppreference.com/w/cpp/atomic
http://en.cppreference.com/w/cpp/atomic/atomic

Anyhow, just a thought at this stage. Other notes:

https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html
https://preshing.com/20130618/atomic-vs-non-atomic-operations
https://homes.cs.washington.edu/~djg/papers/atomjava_tr_may06.pdf
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.221.900&rep=rep1&type=pdf
https://onlinelibrary.wiley.com/doi/pdf/10.1002/cpe.635

[DavePearce]

Migrated from Whiley/WhileyCompiler#649

[DavePearce]

There are some implications around atomic blocks:

• (Acquisition) Upon entering an atomic block, the lock for each potentially modified variable must be acquired. An interesting question is how this is done safely.
• (Locks) Therefore, every global variable and heap allocated data requires a lock.
• (Methods) Furthermore, calling out to a method within an atomic block requires that method to have appropriately declared what global state it can access (e.g. via a modifies clause or similar). The default state for a method is that it could modify any global state, but we cannot possibly handle this.
• (Reasoning) Realistically, we can only reason about changes to global data within an atomic block.

[DavePearce]

@GraemeSmith another one for you

[DavePearce]

An interesting issue arises if we permit writes to global variables outside of atomic blocks (even if these are themselves atomic #45). Therefore, making this proposal and that for reading / writing global variables atomically coherent requires care:

• (Atomic Modified) We could require that only globals marked as atomic be accessed in an atomic block. Other global variables can be read / written at any time.
• (Lock Everything) Alternatively, we could simply require that all reads / writes to global variables outside an atomic block acquire a lock first.
• (Static Analysis) Another alternative would be to rely on static analysis to determine which global variables are used in atomic blocks. They then need to be locked, whilst others don't.

Presumably, the latter option is less efficient. Furthermore, it prohibits attempts at writing lock-free data structures.

[DavePearce]

Another relevant issue here arises from ideas contained in the paper:

Checking concise specifications for multi-threaded software, JOT 2004

In this paper, a property accessible_if is introduce to restrict when a variable can be accessed. This helps in several ways:

• Guarantees. Whilst we can implement locks using atomic blocks, we cannot easily prohibit incorrect usage. For example, one could take a lock at any time by simply writing to its controlling variable. Using an accessibility predicate we can control when it can be written.
• Monitors. The general plan for shared global variables would be to require a separate monitor for each one. However, using an accessibility predicate we can indicate when one shared variable is controlled by another (hence, doesn't need another monitor).

In general, I think it makes sense to think about these accessibility predicates more like "ownership" predicates. Potentially we might want to separate out reading / writing as well, though I think writing is the most important.

Using this, we can further restrict what is permitted within an atomic block. We can