Unlocking Data Race Freedom in Task Parallel Programs

Proving Data Race Freedom in Task Parallel Programs Using a Weaker Partial Order Benjamin Ogles, Peter Aldous, and Eric Mercer Brigham Young University

Data Race Two unordered accesses to the same location with at least one being a write Input Sequentially consistent memory model Single lock for critical all sections

Many Schedules To Consider for Proof Parallel Program Input All Histories Generator Massive Set of Possible Histories Infeasible to check every history

Happens-before Soundly Partitions Histories All Histories 1 4 3 2 5 6 7 9 8 Check representative from each partition for proof

Prove Does-not-Commute Soundly Weakens Happens-before All Histories 2 1 3 4 5 Check many fewer representatives for proof

Execution Histories T0 Acq l T0 Read x T0 Rel l T1 Acq l T1 Write x T1 Rel l T0 Write y

Execution Histories T0 Acq l T0 Read x T0 Rel l T1 Acq l T1 Write x T1 Rel l T0 Write y T1 Acq l T1 Write x T1 Rel l T0 Acq l T0 Read x T0 Rel l T0 Write y

Execution Histories T0 T1 T0 T1 Acq l Write x Rel l Acq l Read x Rel l Acq l Read x Rel l Write y Acq l Write x Rel l Write y

History Determines Value Read T0 T1 T0 T1 Acq l Write x Rel l Acq l Read x Rel l Acq l Read x Rel l Write y Acq l Write x Rel l Write y Must consider each interesting history

Data Race Witness T0 Acq l Write y Rel l Read x T1 Write x Acq l Read y Rel l

Witness Trace T0 Acq l Write y Rel l Read x T1 Write x Acq l Read y Rel l

Witness Trace is Not Always the History Observed T0 Acq l Write y Rel l T1 Write x Acq l Read y Rel l Read x

Infer Witness from Non-witness T0 T1 T0 T1 Acq l Write y Rel l Write x Acq l Read y Rel l Read x

Infer Witness from Non-witness T0 T1 T0 Acq l Write y Rel l T1 Acq l Write y Rel l Write x Acq l Read y Rel l Write x Read x Acq l Read y Rel l Read x

Must Preserve Thread Order T0 T1 T0 Acq l Write y Rel l T1 Acq l Write y Rel l Write x Acq l Read y Rel l Write x Read x Acq l Read y Rel l Read x

Reads See Same Writes T0 T1 T0 Acq l Write y Rel l T1 Acq l Write y Rel l Write x Acq l Read y Rel l Write x Read x Acq l Read y Rel l Read x

Happens-Before (Lamport 1978) T0 Acq l Write y Rel l T1 Write x Acq l Read y Rel l Read x

Naturally Preserves the Properties T0 Acq l Write y Rel l T1 Write x Read x Acq l Read y Rel l

Feasible Histories

Observe a History Feasible Histories

Infer Other Histories from Partial Order Feasible Histories

Weaken Partial Order To Infer More Feasible Histories But may infer infeasible histories that data race

Sound Weakened Partial Orders Feasible Histories Data-race in infeasible implies real exists with same race

Happens-before Sound to First Race T0 ... Acq l Write y Rel l T1 ... Read x Write x Acq l Read y Rel l ... ...

Anything After Witness is Unsound T0 ... Acq l Write y Rel l Write x T1 ... Read x Acq l Read y Rel l ... ...

Weaken To Make Bigger Partitions Feasible Histories And only worry about first data race

Does-not-Commute (Roemer 2019) T0 Acq l Write x Rel l Write z Acq l Write y Rel l T1 Acq l Write x Rel l Read z Only order Rel with conflicting event in critical sections

Infers Witness from Original History T0 Acq l Write x Rel l T1 Acq l Write x Rel l Write z Read z Acq l Write y Rel l

Happens Before Cannot Infer Witness T0 Acq l Write x Rel l Write z Acq l Write y Rel l T1 Acq l Write x Rel l Read z

But Does-not-Commute Also Infers Infeasible Histories T0 Acq l Write x Rel l Write z Acq l Write y T1 Acq l Write x Rel l Rel l Read z Not an issue if inferred data race is real

Mechanize Proof in Coq A feasible trace exists to witness the first data-race inferred by the does-not- commute partial order from an observed history The inferred non-feasible histories are the rub

Causal Events T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y Anything does-not-commute ordered before race events

Witness Order Strengthens Does- not-commute on Causal Events T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y Anything does-not-commute ordered before race events

Witness Order Strengthens Does- not-commute on Causal Events T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y Plus Rel to Acq event orders from observed history

Witness Order Strengthens Does- not-commute on Causal Events T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y And any Acq with no matching release after all other Rels

Witness Order is Anti-symmetric T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y Thus can be extended to a total order witness trace

Lemma Relies on Single Lock Property and Causal Events to Avoid Cycles T0 T1 Acq l Read x Rel l Acq l Write x Read y Rel l Acq l Read z Rel l Write y Only one unmatched Acq may exist but matched Rel not causal so no cycle

Extend Witness Order to Total Order T0 T1 Acq l Read x Rel l Acq l Read z Rel l Acq l Write x It antisymmetric after all

Add in the data race T0 T1 Acq l Read x Rel l Acq l Read z Rel l Acq l Write x Read y Write y

Guaranteed to be Enabled T0 T1 Acq l Read x Rel l Acq l Read z Rel l Acq l Write x Read y Write y Because it includes all causal events

Guaranteed to be Enabled T0 T1 Acq l Read x Rel l Acq l Read z Rel l Acq l Write x Read y Write y And keeps thread order, locking, writes-to-reads, and first race

Result The Does-not-Commute relation is sound for single-lock programs. But is it complete---infers race if one is possible?

Does-not-commute Cannot Infer this data-race T0 T1 Acq l Write x Rel l Acq l Write x Rel l Write x

Even Though it has a Witness Trace T0 T1 Acq l Write x Rel l Acq l Write x Write x Rel l

And Would Have Been Inferred From a Different Observed History T0 T1 Acq l Write x Rel l Write x Acq l Write x Rel l

Weak Does-not-Commute T0 Acq l Write x Rel l T1 Acq l Write x Rel l Write x Doesn t order write-only conflicts

But Now Which Writes Races? T0 Acq l Write x Rel l T1 Acq l Write x Rel l Write x

Strengthen Data Race Definition T0 Acq l Write x Rel l T1 Acq l Write x Rel l Write x Two conflicting events and at least one not in a critical section

Weak-Does-not-Commute Sound with the strengthened definition of data race But we don t know if it is complete

Model Checking T0 T0 T1 Read y T1 Acq l Read x Rel l Acq l Write x Rel l ... ... Dynamic Partial Order Reduction (Flanagan 2005)