Fix coherent-read-read issue by changing from last_seen_order_ to first_seen_order_

[doronrk]

I noticed that relacy can be made not to respect coherent read-read due to the fact that each record maintains last seen order instead of first seen order. I have added a test case in test/memory_order.hpp to show how this can happen. Maintaining first seen order instead of last seen order prevents two loads from getting entries in the modification history that are backwards relative to the ordering of the loads.

I don't believe any other logic is impacted by switching from first to last seen. The only other place last_seen is used is in setting the value of aba in atomic_rmw. The existing comparison for aba is effectively comparing against (timestamp_t)-1, so it should not matter whether first or last seen is used. I've also updated the comparison to reflect this.

Am I missing an important reason why last seen order must be maintained instead of first seen order? If I am, is there a way to fix the coherent read-read issue?

Thanks!

[dvyukov]

Hi Doron,

I need to admit that I don't remember much about the code at this point, but I will try to recall details. Why coherent_read_read_test test should work? Store to x does not happen-before store to y as far as I see, so thread 3 can load any value. What I am missing?

As far as I see last_seenorder is the right order to use for both get_load_index and ABA predicate. Using first_seenorder for get_load_index violates 1.10/16:

If a value computation A of an atomic object M happens before a value computation B of M, and A takes
its value from a side effect X on M, then the value computed by B shall either be the value stored by X or
the value stored by a side effect Y on M, where Y follows X in the modification order of M.

Which means subsequent loads of an atomic variable in the same thread must return either the same of newer values, but never go backwards. Using first_seenorder allows seeing older values.

In the note to 1.10/16 I see that it's called "read-read coherence", so maybe that's the rule that you meant. But this rules talks about a single atomic variable only, it does not say anything about relations between different variables.

[doronrk]

Hi Dmitry,

Thanks for looking at my pull request so quickly.

Regarding why the coherent_read_read_test should work: Not sure if you are familiar with CppMem tool (http://svr-pes20-cppmem.cl.cam.ac.uk/cppmem/), but this is how I confirmed that my test case shows a violation of the standard. If you paste the following expression of the coherent_read_read_test in CppMem's specialized language it explains the violation (I'll explain in my own words below as well):

int main() {
  atomic_int x = 0;
  atomic_int y = 0;
  {{{
  {
    x.store(1, memory_order_relaxed);
  }
  |||
  {
    x.load(memory_order_relaxed).readsvalue(1);
    y.store(1, memory_order_release);
  }
  |||
  {
    y.load(memory_order_acquire).readsvalue(1);
    x.load(memory_order_relaxed).readsvalue(0);
  }
  }}};
  return 0;
}

Re: "But this rules talks about a single atomic variable only, it does not say anything about relations between different variables." Agreed, but the non-coherent reads addressed by the test are only against the variable x. The variable y only exists to facilitate inter-thread synchronization between threads 1 and 2. Specifically, 0 appears before 1 in x's modification order. The load of x by thread 1 on line 21 happens before the load of x by thread 2 on line 30. Because thread 1's load of x happens before thread 2's load of x, thread 2's load must not get a value older than thread 1's load in the modification order (this is basically what coherent-read-read i.e. 1.10/16 is saying).

Re: "subsequent loads of an atomic variable in the same thread must return either the same of newer values, but never go backwards. Using first_seenorder allows seeing older values." first/last_seenorder is a per-record data structure, not a per buffer data structure. So as get_load_index probes older and older records, it will still break from the loop as soon as it encounters the last valid record in the modification order. The difference is that subsequent loads of the same record by the same thread do not update first_seenorder for that record - only the first load of each record by each thread matters. In fact, overwriting this value with a more recent timestamp for a subsequent read of the same record by the same thread (line 25 of the test) is what causes get_load_index to return a value that is too old in the modification order for the next thread that loads the atomic.

[doronrk]

Oh I forgot to address the ABA part.

The current comparison for aba is:

        timestamp_t const last_seen = var.history_[var.current_index_ % atomic_history_size].last_seen_order_[index_];
        aba = (last_seen > own_acq_rel_order_);

The only time last_seen > own_acq_relorder is when last_seen == (timestamp_t)-1 because last_seen is only written in two places: (timestamp_t)-1 on initialization, and own_acq_relorder on loads. It should not matter whether first_seen or last_seen is compared against (timestamp_t)-1, because the comparison is essentially asking "has this record been seen at all".

Conceptually, I don't actually fully understand why this comparison is sufficient to set the value of aba, but this is what the code seems to be doing. It seems you would also need to do a little bit more work to actually compare the value returned by the last load for the current thread against the one about to be returned. This, combined with the fact that the loading thread has not yet loaded the current record seems closer to determining the ABA problem. However, I've definitely spent less time thinking about this than I have just ensuring the code behaves the same way as before, so please let me know if I'm off base here.

Thanks!

[dvyukov]

Okay, this makes sense. I confused meaning of last_seenorder, I thought it is per-variable thing meaning "what value we last saw", but this is per variable value thing meaning "when we saw this particular value".

I will take closer look tomorrow.

Meanwhile please use bracket style consistent with the rest of the code: (1) { on a separate line, (2) no {} for single-statement if/for.

Thanks.

[doronrk]

Sounds good! I'll update the bracket style.

[doronrk]

Fixed the bracket issue. Let me know if you'd rather have this just be 1 commit and I can squash and force push.

[doronrk]

I added the read-read coherence comment. Please let me know if I can make any other improvements.

[dvyukov]

Thanks for bearing with me. Merging.