[Question] understanding of BoC

[wyhallenwu]

In BoC, . A behaviour b will happen before another behavior b' iff b and b' requires overlapping sets of cowns, and b is spawned before b'. But I'm curious about the nested case, for example:

when(c1,c2) {
         when(c2, c3)
}

when(c3, c4) {
....
}

Is the DAG looks like when(c1,c2) -> when(c2, c3) -> when(c3, c4). Cause the spawned when(c2,c3) is in the thunk of when(c1,c2). Is it possible that the when(c3,c4) happens before when(c2,c3)? Or if there is something that I misunderstand?

[kingdoctor123]

In fact, happens-before is much stricter than simply "spawned before". For more information, you can read https://en.wikipedia.org/wiki/Happened-before. To put it simply, you can understand it as a causal order between operations.

when(c1, c2) { // b1
    when(c2, c3) { ... } // b2
}

when(c3, c4) { // b3
}

In your example,

• b1 happens-before b3, since they are scheduled sequentially on a same thread. Due to this causality, it is never the case that b3 is executed earlier than b1.
• b1 happens-before b2, since b2 can be scheduled only after b1 is scheduled and executed. Due to this causality, it is never the case that b2 is executed earlier than b1.
• But, we cannot say either b2 happens-before b3 or b3 happens-before b2, because there are no causal ordering between them. Since there is no causality, b2 can be executed earlier than b1, and b1 can be executed earlier than b1.

However, in the following case, you have b3 happens-before b2.

let x = false; // x: AtomicBool
when(c1, c2) { // b1
    if x.load(SeqCst) {
        when(c2, c3) { ... } // b2
    }
}

when(c3, c4) { // b3
}
x.store(true, SeqCst);

In this code, b3 happens-before b2 holds, since b2 is scheduled only if x.store(true, SeqCst) is executed before x.load(SeqCst). This gives a causal order between b2 and b3.

[wyhallenwu]

Thank you for your explanation, just for double check if I understand it. In the hw boc.rs test case boc::boc.

    when!(c1, c2; g1, g2; { \\b1
        *g1 += 1;
        *g2 += 1;
        when!(c3, c2; g3, g2; { \\b2
            *g2 += 1;
            *g3 = true;
        });
    });

    when!(c1, c2_, c3_; g1, g2, g3; { \\b3
        assert_eq!(*g1, 1);
        assert_eq!(*g2, if *g3 { 2 } else { 1 });
        finish_sender.send(()).unwrap();
    });

In this case, the b1 happens before b2 and b3. b2 can be only scheduled after b1 scheduled and excuted. but there is no certain order between b2 and b3 cause they don't have overlapping cowns.

[kingdoctor123]

b2 and b3 do have overlapping cowns (note that c2_ is a cloned version of c2 and c3_ is a cloned version of c3). However, since they do not have causal order, b2 and b3 can be executed in any order.