1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
use super::super::support::vv;
use crate::metis::with_scope;
#[test]
fn test_created_order_hazard_through_the_scope() {
// The created-order hazard (PRD 0013), reproduced THROUGH the branded API
// the safe way. This mirrors `test_restriction_creates_order` in the
// version_vector examples: `a` and `b` are concurrent over the full base,
// but restrict to an ordered pair over the sub-roster {1} that drops the
// witness station 2.
let a = vv(&[(1, 3), (2, 1)]);
let b = vv(&[(1, 1), (2, 4)]);
assert!(a.concurrent(&b));
// Over the roster {1}, `b` precedes `a`: a scoped order verdict, readable
// and sound only inside the scope. `concurrent_globally` reports false in
// this direction (the restrictions are ordered, not concurrent), which is
// exactly the created-order hazard the brand keeps from escaping.
let scoped_order_holds = with_scope([1u32], |scope| {
let ra = scope.restrict(&a);
let rb = scope.restrict(&b);
assert!(rb.happens_before(&ra)); // fabricated by forgetting station 2
assert!(!rb.concurrent_globally(&ra)); // ordered, so not concurrent
// The scoped verdict is readable; the escape is deliberate.
let forgotten_a = ra.forget();
// After forget, the branding is gone and the global read is honest:
// the ORIGINALS are still concurrent, the scoped order notwithstanding.
assert!(forgotten_a.concurrent(&b));
rb.happens_before(&scope.restrict(&a))
});
assert!(scoped_order_holds);
}
#[test]
fn test_concurrency_reflects_globally_through_the_scope() {
// The reflection direction is sound: when the SCOPED restrictions are
// concurrent, `concurrent_globally` is true and the originals were already
// concurrent (the two leading stations survive in the roster {1, 2}).
let a = vv(&[(1, 3), (2, 1)]);
let b = vv(&[(1, 1), (2, 4)]);
assert!(a.concurrent(&b));
let reflected = with_scope([1u32, 2], |scope| {
let ra = scope.restrict(&a);
let rb = scope.restrict(&b);
// Over {1, 2} the restrictions disagree in both directions: concurrent.
assert!(ra.concurrent_globally(&rb));
ra.concurrent_globally(&rb)
});
assert!(reflected);
// The unbranded bool that escaped certifies the originals are concurrent.
assert!(a.concurrent(&b));
}