SC for DRF
sequential consistency for data race freedom。DRF-SC。data 競合の無い時の逐次一貫性
programming 言語に於けるよくある memory model
逐次一貫性 (sequential consistency。順次整合性。逐次整合性)
data 競合 (data race)
data race
type 1 data race
Two memory operations conflict if they access the same memory location, and at least one of them is a store, atomic store, or atomic read-modify-write operation. In a sequentially consistent execution, two memory operations from different threads form a type 1 data race if they conflict, at least one of them is a data operation, and they are adjacent in$ <_T(i.e., they may be executed concurrently).
We can now specify the C++ memory model simply as: If a program (on a given input) has a sequentially consistent execution with a (type 1) data race, then its behavior is undefined.
Otherwise, the program (on the same input) behaves according to one if its sequentially consistent executions.
type 2 data race
A consistent execution contains a type 2 data race if two data accesses to the same memory location are unordered by happens-before. We can now specify the C++ memory model simply as: If a program (on a given input) has a consistent execution with a (type 2) data race, then its behavior is undefined.
Otherwise, the program (on the same input) behaves according to one if its consistent executions.
7. Sequential Consistency for Data-Race-Free Programs (SC for DRF) THEOREM 7.1. The model defined in Section 6 provides sequential consistency to programs whose consistent executions do not contain a type 2 data race.
8. Equivalence of Race Definitions
THEOREM 8.1. If a program allows a type 2 data race in a consistent execution, then there exists a sequentially consistent execution, with two conflicting actions, neither of which happens before the other.
THEOREM 8.2. A program allows a type 2 data race on a given input if and only if there exists a sequentially consistent execution in which two unordered conflicting actions are adjacent in the sequential interleaving, i.e. it allows a type 1 data race.
Requirement 1
The memory operations in each goroutine must correspond to a correct sequential execution of that goroutine, given the values read from and written to memory. That execution must be consistent with the sequenced before relation, defined as the partial order (半順序 (poset)) requirements set out by the Go language specification for Go's control flow constructs as well as the order of evaluation for expressions. A Go program execution is modeled as a set of goroutine executions, together with a mapping$ Wthat specifies the write-like operation that each read-like operation reads from. (Multiple executions of the same program can have different program executions.)
Requirement 2
For a given program execution, the mapping$ W, when limited to synchronizing operations, must be explainable by some implicit total order (全順序) of the synchronizing operations that is consistent with sequencing and the values read and written by those operations. The synchronized before relation is a partial order (半順序 (poset)) on synchronizing memory operations, derived from$ W. If a synchronizing read-like memory operation r observes a synchronizing write-like memory operation$ w(that is, if $ W(r)=r), then$ wis synchronized before$ r. Informally, the synchronized before relation is a subset of the implied total order (全順序) mentioned in the previous paragraph, limited to the information that$ Wdirectly observes. The happens before relation is defined as the transitive closure of the union of the sequenced before and synchronized before relations.
Requirement 3
For an ordinary (non-synchronizing) data read$ ron a memory location$ x,$ W(r)must be a write w that is visible to r, where visible means that both of the following hold:
1. $ whappens before$ r.
2. $ wdoes not happen before any other write$ w'(to$ x) that happens before$ r.
A read-write data race on memory location$ xconsists of a read-like memory operation$ ron$ xand a write-like memory operation$ won$ x, at least one of which is non-synchronizing, which are unordered by happens before (that is, neither$ rhappens before$ wnor$ whappens before$ r).
A write-write data race on memory location$ xconsists of two write-like memory operations w and$ w'on$ x, at least one of which is non-synchronizing, which are unordered by happens before.