Skip to content

ParkingLot: symmetric F^sc on park side (mirror of ff7ab9d) #2649

Description

@vijay-nagarajan

ParkingLot.h lines 264 (A) and 300-304 (B):

// A: Must be seq_cst.  Matches B.                     
bucket.count_.fetch_add(1, std::memory_order_seq_cst);                                                                                         
...                                         
// B: Must be seq_cst.  Matches A.  If true, A *must* see in seq_cst                                                                           
// order any atomic updates in toPark() (and matching updates that
// happen before unpark is called)                                                                                                             
std::atomic_thread_fence(std::memory_order_seq_cst);
if (bucket.count_.load(std::memory_order_seq_cst) == 0) { return; }                                                                            

Commit ff7ab9d added the seq_cst fence on the unpark side so the client's store before unpark() is lifted into C/C++ SC axiom, regardless of its memory order. The symmetric situation on the park side appears unaddressed: between A's SC fetch_add and the client-supplied toPark() callback's predicate read there is no F^sc. If the client reads the predicate with memory_order_acquire (or weaker), the SC cycle does not close under C/C++ memory ordering rules and the lost-wakeup outcome is reachable.

Reduced 2-thread litmus (waiter + waker):

{ count = 0; pred = 0; }                                                                                                                       
P0 (count, pred) {  // waiter                          
  int x = atomic_fetch_add_explicit(count, 1, memory_order_seq_cst);
  int p = atomic_load_explicit(pred, memory_order_acquire);
}                                                                                                                                              
P1 (count, pred) {  // waker
  atomic_store_explicit(pred, 1, memory_order_release);                                                                                        
  atomic_thread_fence(memory_order_seq_cst);           
  int c = atomic_load_explicit(count, memory_order_seq_cst);                                                                                   
}                                                                                                                                              
exists (0:p=0 /\ 1:c=0 /\ 0:x=0)        

herd7 -model rc11.cat: Ok, 1/4 states reach (p=0, c=0).

Note: the ff7ab9d commit summary's own example litmus shows thread 2 (the park-side analog) using seq_cst for both the fetch_add and the subsequent load. Under that assumption no fence on the park side is needed. In practice, toPark() lambdas could read the wake-condition predicate with memory_order_acquire or weaker, violating that implicit assumption, and the comment at B does not state it.

Proposed patch (mirrors ff7ab9d)

   {                                                                                                                                           
     // A: Must be seq_cst.  Matches B.
     bucket.count_.fetch_add(1, std::memory_order_seq_cst);                                                                                    
+    // Symmetric to the fence at B (commit ff7ab9d): lifts the client's
+    // atomic reads inside toPark() so the
+    // guarantee documented at B holds regardless of the client's
+    // memory order on those reads.                                                                                                           
+    std::atomic_thread_fence(std::memory_order_seq_cst);
                                                                                                                                               
     std::unique_lock bucketLock(bucket.mutex_);       
                                                                                                                                               
     if (!std::forward<ToPark>(toPark)()) {            

With this fence the same litmus (with the new park-side fence in P0) is No, 0/3 states reach the bad outcome under RC11. Verified with herd7.

Open to maintainer judgment. A doc-only alternative -- requiring client toPark() reads to use seq_cst-- also works, but the symmetric-fence patch matches the precedent set by ff7ab9d and removes a memory-order requirement from the caller side.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type
    No fields configured for issues without a type.

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions