BPlusTree.Lock

enum Lock[_: Eff]Source

case Lock(java.util.concurrent.locks.StampedLock)

The purpose of Lock is to provide a thin wrapper around Java's StampedLock without the IO effect. The lock is optimistic in the sense that reads are performed by reading the values and only afterwards verifying that no other thread has changed the values. Only annotating a region effect to StampedLock is safe, since it can only non-deterministically block a thread for some ( potentially infinite) amount of time. This is allowed under non-effectful behavior.

One possible danger, introduced by StampedLock, is handled by a null-check in binarySearch. Consider the following example where everything is initialized to 0: Thread 1 executes {a = 2; b = 3} Thread 2 executes {c = a; d = b} The question is what can c and d be? It depends on the JVM, but can be any of: {c = 2, d = 3}, {c = 0, d = 0}, {c = 2, d = 0}, {c = 0, d = 3} The last follows from the fact that the JVM can reorder statements under some requirements. The requirements are roughly that the new 'code' should be equivalent on a single-threaded machine and there are no happens-before relations which link to other threads preventing the reordering. If either variable were volatile we might avoid this, but volatile is expensive (and not in Flix).

For us, this means that {array[size] = 5; size++} can be reordered to {oldSize = size++; array[oldSize] = 5}. Another thread reading may then see the increase of size and try to access that position getting null. This has not happened in our experiments, but we wish to handle the case. The risk is in binarySearch and we therefore check whether any value read is null and if so 'aborts'.

For Java's memory model see: https://docs.oracle.com/javase/specs/jls/se8/html/jls-17.html#jls-17.4

Definitions

def isLocked(lock: Lock[r]): Bool \ r Source

Returns true if lock is currently held by a thread.

Only supposed to be used for testing.

def mkLock(_: Region[r]): Lock[r] \ r Source

Returns a fresh lock.

def tryConvertToWrite(stamp: Int64, lock: Lock[r]): Int64 \ r Source

Attempt to upgrade stamp on lock to a write-lock on lock. The returned stamp cannot be invalidated if it was valid when issued.

This operation is non-blocking.

def tryReadLock(lock: Lock[r]): Int64 \ r Source

Return an optimistic stamp on lock which can be used in valid to assert that no thread has taken a write lock since stamp was issued.

This operation is non-blocking.

def unlockWrite(stamp: Int64, lock: Lock[r]): Unit \ r Source

Unlock lock with the issued write-stamp, stamp.

This operation is non-blocking.

def valid(stamp: Int64, lock: Lock[r]): Bool \ r Source

Returns true if stamp is still valid on lock, meaning no thread has acquired a write-lock on lock since stamp was issued.

This operation is non-blocking.

def writeLock(lock: Lock[r]): Int64 \ r Source

Lock lock and returns the stamp.

This operation is blocking.

def yieldBasedOn(lock: Lock[r]): Unit \ r Source

Wait for lock to be unlocked by the current holder of the write-lock on it.

Why:

Virtual threads can exhibit weird behaviour when using all physical threads and using locking. Without this the threads using optimistic reading will never be removed from the physical thread. Meanwhile a thread that holds the lock will never get to run and we have a deadlock. Progress can happen, but it appears to be extremely unlikely. To fix this call a blocking operation which makes the JVM remove the virtual threads from the physical threads allowing the lock-holder to unlock.

For a better explanation see Netflix's encounter of a similar problem: https://netflixtechblog.com/java-21-virtual-threads-dude-wheres-my-lock-3052540e231d?gi=128dba0ad426