Undefined Types for Concurrency

[DavePearce]

(see also #35 and #45)

The use of undefined types might also be useful in a concurrent setting. The rough idea is that, if we have a global variable with an undefined type (e.g. ?int) then we don't need atomic reads / writes to that variable. The problem is how we actually use these variables to some useful effect. In particular, since reads and writes are not atomic, reading from a variable of type ?int gives an undefined value (which e.g. could represent some value part way through a write by another thread). However, we can control these values using other atomic variables. The benefit of this is reduced time spent locking when reading or writing data.

The concept of a seqlock is one algorithm that does something like this:

type SeqLock<T> is {
  int count,
  ?T data
} 
// Ensure data defined for even count
where (count % 2) == 0 <==> data is T

atomic method seqlock_write<T>(&SeqLock<T> p, T value)
requires (p->count % 2) == 0:
    // make count uneven
    p->count = p->count + 1
    // write data value
    p->value = value
    // make count even again
    p->count = p->count + 1

method seqlock_read(&SeqLock<T> p) -> (T r):
    //
    int r0
    ?T r1
    //
    do:
      // Wait until writer finished
      do:
        r0 = p->count
      while (r0 % 2) != 0
      // Attempt to read data
      r1 = p->data
      //
    while p->count != r0 
    // when condition false `r1` is defined
    where (r0 == p->count) ==> r1 is T
    //
    return r1 

This algorithm makes sense when we have a small number of writers and a larger number of readers. The key is that the readers never acquire locks and busy wait instead of blocking. Furthermore, the invariant is what guarantees that data is defined when the count is even. The loop invariant is probably needed to ensure this would verify (though this really needs to be thought through).

[DavePearce]

@GraemeSmith Final one for now. Note, these are not RFCs yet. But they are precursors to being written up as RFCs. You can see all the current RFCs here: https://github.com/Whiley/RFCs/tree/master/text

[DavePearce]

@GraemeSmith In above example, have made seqlock_write() an atomic method meaning it cannot be interrupted. I think this is necessary in a truly concurrent setting, right?

[DavePearce]

@GraemeSmith Hmmmm, does that make sense? If seqlock_write() cannot be interrupted then seqlock_read() would never see count as being non-even. Needs more thought!

[GraemeSmith]

@DavePearce seqlock_write shouldn't be interruptible by other writer threads, but it can be interrupted by reader threads. This is usually implemented using a spinlock which the writer must acquire before proceeding.

[DavePearce]

Issues with the implementation of SeqLock<T> above are:

• Making seqlock_write() atomic is not consistent with the original implementation. In the original, the goal is to prevent writers from racing but not to prevent readers from racing. Specifically, readers don't acquire a lock as this would starve the writers.
• The original implementation uses a spinlock in the write method to prevent multiple writers. A spinlock could be implemented using an atomic block as e.g. a library primitive.
• Another option would be to have a synchronized keyword which would basically compile down to a spinlock and achieve the same thing. This would be different from an atomic block.

[DavePearce]

Another interesting algorithm is the Treiber Stack. Here's a first approximation of a Whiley implementation:

// Value-oriented linked list
type Node<T> is { LinkedList<T> next, T data }
type LinkedList<T> is null | Node<T>
// Triber stack with reference to list
type Stack<T> is { &LinkedList<T> head }

method treiber_push<T>(Stack<T> stack, T item):
   Node<T> newHead = { next: null, data: item }
   Node<T> oldHead
   do:
      oldHead = stack.head        // Does this force a copy?
      newHead.next = oldHead  // oldHead has multiple owners here
   while !CAS(stack.head,oldHead,newHead)

One of the assumptions here is that pointer reads are atomic and, hence, there is no need for an undefined type (as with the seqlock).

The key question here is whether or not the assignment forces a copy. Because this is recursive structure, it must be implemented using a pointer under-the-hood. However, stack.head does have multiple owners at one point.

Under a simple ownership scheme, we have the following:

• A single bit of ownership data is associated with unbounded data structures.
• When multiple readers are created for such a structure, this bit is unset.
• When writing to such a data structure, if the bit is unset we must clone the whole structure.
• Therefore, in the above, we actually do avoid cloning.

One question is how deallocation of a non-unique data structure is managed.

NOTE: the challenge here is that it's not really clear what we could verify in Whiley about this data structure. Realistically, we want to reason over some kind of linearizability.

[DavePearce]

Other possible algorithms to consider:

• https://en.wikipedia.org/wiki/Peterson%27s_algorithm
• https://en.wikipedia.org/wiki/Array_Based_Queuing_Locks
• Possibly look in "The art of multiprocessor programming".

[GraemeSmith]

Other mutual exclusion algorithms include Dekker's
https://en.wikipedia.org/wiki/Dekker%27s_algorithm
and Burns's
https://www.sciencedirect.com/science/article/pii/S0890540183710655

But these, like Peterson's, aren't used in practice since a programmer wanting mutual exclusion would normally use a lock (if available in the language's library) or implement a lock using an atomic hardware primitive (like CAS, TAS, etc).

[DavePearce]

Other interesting things to look at:

• Chase-Lev Deque (array-based)
• Non-blocking array-based algorithms for stacks and queues (MSc Thesis). www.cse.yorku.ca/~niloo/resources/MScthesis.pdf
• A Scalable Lock-free Stack Algorithm. https://www.cs.bgu.ac.il/~hendlerd/papers/scalable-stack.pdf

[DavePearce]

Another interesting question is how even to implement locks in a sensible fashion. For example, suppose we have:

type Lockable<T> is { mutex lock, T data }
where lock.is_held() ==> data != ?

method lock(&Lockable<T> l)
ensures l.is_held():
   ...

method unlock(&Lockable<T> l)
requires l.is_held():
   ...

The challenge here is that we are looking for some way to express useful things about stuff inbetween a lock() and unlock() pair. Roughly speaking the invariant on Lockable says that: if the lock is held then no one else ever writes to it

[DavePearce]

The trieber stack is interesting because it's really about writing two pointers simultaneously (this is the linearisation point). The pointers being stack.next and newHead.next above. The function is "correct" in some sense if these two values are written atomically (i.e. the writes are not interrupted). This gives us a general framework for thinking about the problem. Consider this:

?int x
?int y

metho m():
   y = x + 1
   assert x < y

The above fails because the two variables x and y could be modified at any point (i.e. be given an arbitrary value as indicated by ?). Somehow we need to be able to reason despite this, and local variables provide the key mechanism as they are thread-local. Therefore, you end up with some implication like:

(lvar == value) ==> x < y

Here, lval is a local variable and we're using it to determine when the atomic write has occurred.