Nondeterminism#

thread interleaving#

interleaving semantics： 将多线程的指令交替组合成好像是单线程执行一样。

不同线程间的Load/store指令是穿插执行的，导致最终的行为有多种多样的可能。

static COUNTER = AtomicUsize::new(0);
// thread A & B
let c = COUNTER.load();
COUNTER.store(c + 1);

如上示例，两个线程A和B同时对COUNTER进行+1操作，预期结果当然是2。但是由于线程调度的不确定性可能出现如下的执行顺序：

[COUNTER=0] A load, B load, A store, B store [COUNTER=1]

导致结果不符合预期。

解决方案#

使用原子的reading & writing，禁止掉这种不符预期的执行顺序。

// thread A & B
let c = COUNTER.fetch_and_add(1);
  • “Read-modify-write”, e.g. swap, compare-and-swap, fetch-and-add

reordering#

同一个线程中的指令会因为硬件和编译器的优化发生指令重排。

DATA = 42;       ||   if FLAG.load() {
FLAG.store(1);   ||       assert(DATA == 42);
                 ||   }

如上图示例，预期是当FLAG.load()为1时，DATA == 42。但是因为指令重排，左边线程中，FLAG.store(1)可能发生在赋值语句前面；右边线程中assert语句也可能发生在if语句前面。

Relaxed behaviors： 观察到的行为不在任意一种 interleaving semeantics 中。

解决方案#

使用ordering primitives禁止这种重排。

  • Fence：在指令之间加上栅栏（fence），禁止越过栅栏重排指令。

    DATA = 42;                ||   if FLAG.load(relaxed) {
fence(SC);                ||       fence(SC);
FLAG.store(1, relaxed);   ||       assert(DATA == 42);  }
    • SC fence: forbidding any reordering across itself
    • Relaxed: imposing no orderings

  • Access ordering：FLAG.store(1, release) and FLAG.load(acquire)

    DATA = 42;                ||   if FLAG.load(acquire) {
FLAG.store(1, release);   ||       assert(DATA == 42);
                          ||   }
    • Release store: forbidding reordering itself w/ earlier instructions
    • Acquire load: forbidding reordering itself w/ later instructions

modeling relaxed behaviors & orderings#

  • Approach 1: disallowing SMAs altogether
    • DRF (data-race freedom): w/o SMAs, no relaxed behaviors happen.
    • Problem: SMAs are essential
  • Approach 2: constraining executions by “axioms”
    • Representing an execution as a value-flow graph, validated w/ axioms
    • Problem 1: not operational semantics (less intuitive)
    • Problem 2: allowing the bad “out-of-thin-air” behaviors
  • Approach 3: modeling reorderings w/ operational semantics