KhronosGroup / KhronosGroup/Vulkan-MemoryModel

Add a note in the spec about causality cycles/out-of-thin air reads

Open
#14 3 comments 0 reactions 0 assignees View on GitHub
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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.