proj-plbook-plChConcurrencySafety

Table of Contents for Programming Languages: a survey

Chapter : Safety for concurrency

caller blocking allows shared memory

If thread A calls a function F in thread B, and blocks until the function in thread B returns control, then the caller can pass in pointers as some of the parameters to F; there is no danger of both threads accessing these pointers simultaneously because thread A is blocked until F completes, provided that F is not allowed to create aliases of these pointers and store them in a memory location that survives past the completion of F (which can be accomplished by a type system that supports uniqueness types) [1].

type systems for concurrency

todo unpack comment by Alexandrescu in [2]

milewski's owner types

and uniqueness types

(see also plChRust)

linear logic

..and that guy's system for uniqueness of each end of a channel

disciplined parallelism

View memory models (event (re)ordering models) in terms of: if you have a shared memory with this model, what is the set of rules that you can follow when programming such that, if you follow those rules, you can imagine that the memory is sequentially consistent?

A data-race-free memory model guarantees sequential consistency for any data-race-free program. A data-race-free memory model might also guarantee sequential consistency for a program with races, as long as the variables participating in races are identified as such (the terminology is that such variables are not 'data variables', but 'synchronization variables').