Add support for tracking thread causality. #38
Conversation
I think hijacking block/unblock won't work for the atomic registers, where the reader has to inherit the clock from the last writer, but there is no blocking. We could try piggybacking clocks on yield's, but since we're likely to remove some yields in the future (since we know we have some redundant ones), I'm worried that change may break causality. So I propose we live with this clunkiness for now, and revisit this later (maybe when we add causality to async). I added a TODO in the spawn method to record this. |
src/sync/atomic/mod.rs
Outdated
| self.inhale_clock(); | ||
| self.exhale_clock(); |
There was a problem hiding this comment.
Why do these happen in the opposite order to in fetch_update?
There was a problem hiding this comment.
Nice catch. It should be the other way around. I also realized fetch_update was wrong -- it was not handling the error case properly. :-(
Fixed both and added comments to explain.
There was a problem hiding this comment.
Also added a new test clock_fetch_update to reveal the fetch_update bug. For the other one, I think the way I had it wasn't a bug, but reordering the steps is more consistent with translating the swap to load/store.
src/runtime/task/mod.rs
Outdated
| use crate::runtime::thread; | ||
| use crate::runtime::thread::continuation::{ContinuationPool, PooledContinuation}; | ||
| use bitvec::prelude::*; | ||
| use bitvec::vec::BitVec; | ||
| use futures::{task::Waker, Future}; | ||
| use std::cell::RefCell; | ||
| use std::cmp::PartialOrd; |
There was a problem hiding this comment.
Fixed. Why doesn't clippy complain?
There was a problem hiding this comment.
Ah, because it's test code. Guess I should run it with --cfg test.
There was a problem hiding this comment.
For the record, it's cargo clippy --tests. TIL.
This change adds support for tracking causality among thread operations.
We do this in the standard way, by associating a vector clock with each thread.
The i'th element of a thread's vector clock denotes its knowledge of the clock
of thread i. Clocks are partially ordered using a pointwise ordering <.
The main property we want is that for any pair of events p, q:
(p causally precedes q) iff (clock at p < clock at q).
We update the code for thread spawn and join, as well as the various synchronization
objects (Atomics, Barriers, CondVars, Mutexes, RwLocks and mpsc channels) to track
causality by updating vector clocks appropriately.
This change does not currently properly track causality for async interactions;
those will be done in a subsequent PR.
This change adds support for tracking causality among thread operations.
We do this in the standard way, by associating a vector clock with each thread.
The i'th element of a thread's vector clock denotes its knowledge of the clock
of thread i. Clocks are partially ordered using a pointwise ordering <.
The main property we want is that for any pair of events p, q:
(p causally precedes q) iff (clock at p < clock at q).
We update the code for thread spawn and join, as well as the various synchronization
objects (Atomics, Barriers, CondVars, Mutexes, RwLocks and mpsc channels) to track
causality by updating vector clocks appropriately.
This change does not currently properly track causality for async interactions;
those will be done in a subsequent PR.
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 license.