Skip to content

Add compare_exchange-specific tests #7

@gonzalobg

Description

@gonzalobg

Need to add following compare-exchange-specific tests for this section of the spec atomics.ref.ops:

bool compare_exchange_(...);
[...]
If the operation returns true, these operations are atomic read-modify-write operations ([intro.races]) on the value referenced by *ptr. Otherwise, these operations are atomic load operations on that memory.

These operations are only atomic rmw if the operation succeeds.
Otherwise they are loads.

// Test 0: cas always fails -> load -> no release -> no extended release-sequence via rmw -> undefined
int flag = 0;
int data = 0;

// thread 0:
P0(int* data, int* flag) {
    *data = 42; 
    // always fails:
    bool succeeded = atomic_compare_exchange_strong_explicit(flag, 1, 1 memory_order_acq_rel, memory_order_acq_rel);
    atomic_fetch_add_explicit(flag, 1, memory_order_relaxed); // extend release-sequence
}

P1(int* data, int* flag) {
  int r0 = atomic_load_explicit(flag, memory_order_acquire);
  if (r0 == 1) {
     int r1 = *data; // Data race
  }
}

// Undefined behavior
check(undef)
// Test 0: cas always succeeds & idempotent -> release -> extended release-sequence via rmw -> synchronizes-with
int flag = 0;
int data = 0;

// thread 0:
P0(int* data, int* flag) {
    *data = 42; 
    // always succeeds:
    bool succeeded = atomic_compare_exchange_strong_explicit(flag, 0, 0 memory_order_acq_rel, memory_order_acq_rel);
    atomic_fetch_add_explicit(flag, 1, memory_order_relaxed); // extend release-sequence
}

P1(int* data, int* flag) {
  int r0 = atomic_load_explicit(flag, memory_order_acquire);
  if (r0 == 1) {
     int r1 = *data; // well-defined: reads 42 if r0 != 0
  }
}

check(r0 == 0 || (r0 == 1 && r1 == 42))

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions