Model and Reason about RaceSuppose R1(X), W1(X), R2(X), W2(X), are read andwriteoperationsfrom2processorsConsider all execution sequences by interleaving.(a:R1(X))... (b:R2(X))...noconflict(a:R1(X))...(b:W2(X))..conflict(a:W1(X))...(b:R2(X)).conflict(a:W1(X))...(b:W2(X)).....conflictAprogram is race free if any interleaving of theoperations contains no state in which location variablesof two processors are at a conflicting pair of operations
Model and Reason about Race Suppose R1(X), W1(X), R2(X), W2(X), are read and write operations from 2 processors Consider all execution sequences by interleaving .(a:R1(X)).(b:R2(X)). no conflict . (a:R1(X)).(b:W2(X)). conflict . (a:W1(X)).(b:R2(X)). conflict . (a:W1(X)).(b:W2(X)). conflict A program is race free if any interleaving of the operations contains no state in which location variables of two processors are at a conflicting pair of operations
Model and Reason about RaceSuppose O1(X), O2(Y), are two operations from2 processors at locations a and b, the locationvariables of the two processors areaandβFor any interleaving of operations(a:O1(X)... (b:O2(Y)).If O1(X) and O2(Y) are read/write, write/write pairsthen X and Y must be distinct(α=a ^β=b) = X+Y should be an invariant
Model and Reason about Race Suppose O1(X), O2(Y), are two operations from 2 processors at locations a and b, the location variables of the two processors areαandβ For any interleaving of operations . (a:O1(X)). (b:O2(Y)). If O1(X) and O2(Y) are read/write, write/write pairs, then X and Y must be distinct (α=a β=b) XY should be an invariant