This just records the parameter for now, and makes it a distinction
between future values. Shouldn't affect model-checker behavior, except
for the introduction of extra future values: one for each thread which
writes the same value.
We calculate whether the writing thread exists at the time of the future
value and if not, find an ancestor thread which does.
{
/* Do more ambitious checks now that mo is more complete */
if (mo_may_allow(writer, reader)) {
{
/* Do more ambitious checks now that mo is more complete */
if (mo_may_allow(writer, reader)) {
+ Node *node = reader->get_node();
+
+ /* Find an ancestor thread which exists at the time of the reader */
+ Thread *write_thread = get_thread(writer);
+ while (id_to_int(write_thread->get_id()) >= node->get_num_threads())
+ write_thread = write_thread->get_parent();
+
struct future_value fv = {
writer->get_value(),
writer->get_seq_number() + params.maxfuturedelay,
struct future_value fv = {
writer->get_value(),
writer->get_seq_number() + params.maxfuturedelay,
+ write_thread->get_id(),
- if (reader->get_node()->add_future_value(fv))
+ if (node->add_future_value(fv))
set_latest_backtrack(reader);
}
}
set_latest_backtrack(reader);
}
}
{
uint64_t value = fv.value;
modelclock_t expiration = fv.expiration;
{
uint64_t value = fv.value;
modelclock_t expiration = fv.expiration;
+ thread_id_t tid = fv.tid;
int idx = -1; /* Highest index where value is found */
for (unsigned int i = 0; i < future_values.size(); i++) {
int idx = -1; /* Highest index where value is found */
for (unsigned int i = 0; i < future_values.size(); i++) {
- if (future_values[i].value == value) {
+ if (future_values[i].value == value && future_values[i].tid == tid) {
if (expiration <= future_values[i].expiration)
return false;
idx = i;
if (expiration <= future_values[i].expiration)
return false;
idx = i;
struct future_value {
uint64_t value;
modelclock_t expiration;
struct future_value {
uint64_t value;
modelclock_t expiration;