KhronosGroup / KhronosGroup/Vulkan-MemoryModel
Add a note in the spec about causality cycles/out-of-thin air reads
- Dominant language
- C++
- Stars
- 117
- Forks
- 15
- PR merge metrics
- No merged PRs in 30d
Description
This memory model appears to have inherited from C++ the issue of allowing causality cycles (a.k.a. out-of-thin-air reads). For example, the following program (in pseudo-code):
```
Thread 1:
r = load_relaxed(x);
store_relaxed(y, r);
Thread 2:
r2 = load_relaxed(y);
store_relaxed(x, r2);
```
can end with any value in both x and y. This is both unwanted (I don't know of any hardware that can actually write 42 in both x and y, with no reference to 42 anywhere in the program) and rather fundamental to the C++ style of axiomatic models. Fixing this in the model is way out-of-scope (it is a hard problem that academia has been trying to fix for several years, and the only solution I consider satisfactory rewrites the entire model in a different style), but we could include a comment similar to that in the C++ spec (note 9 in section 29.3 of http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2014/n4296.pdf):
> 9 Implementations should ensure that no “out-of-thin-air” values are computed that circularly depend on their own computation.
> [ Note: For example, with x and y initially zero,
> // Thread 1:
> r1 = y.load(memory_order_relaxed);
> x.store(r1, memory_order_relaxed);
> // Thread 2:
> r2 = x.load(memory_order_relaxed);
> y.store(r2, memory_order_relaxed);
> should not produce r1 == r2 == 42, since the store of 42 to y is only possible if the store to x stores 42, which circularly depends on the store to y storing 42. Note that without this restriction, such an execution ispossible. —endnote]
Contributor guide
No contributing guide indexed for this repository
Research direction
Start with issue #14 and compare the model's treatment of relaxed loads and stores with C++ N4296 §29.3 note 9. Done means the specification includes a clear note about causality cycles and out-of-thin-air values, using the supplied two-thread example or equivalent.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- cpp
- Domain
- documentation
- Issue type
- Documentation
- Difficulty
- 2/5
- Estimated time
- 1-3 hours
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100