HPC Concurrency Verification Tools
Project Discussions
Overview of what you'll learn today
Keep in mind that
Overview of what you'll learn today
What are observable effects of data races?
I'm sure the term "data race" is not new to most of you.
What do you understand by it?
Most would say "introduces nondeterminism"
What are observable effects of data races?
Most would say "introduces nondeterminism"
Well, if the desired behavior is deterministic, then seeing
nondeterminstic outcomes is bad
NOT TRUE!
Many programs are supposed to produce nondeterministic outputs!
Example
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
Example
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
Notice that there is nondeterminism!
Even if we put a "lock / unlock" surrounding each statement (which eliminates all races), this can be observed!
Example
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
Thus, please don't hereafter say that "when there is a data race, the results will be nondeterminstic" and pretend that that's it, and that's bad!
Because that may be what the final semantics requires (to see all these values) … as in an OS
Example : one more twist
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
x == 5 ? How can this be seen?
Example : one more twist
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
x == 5 ?
Answer: When the compiler moves the
y := y + 1 before the x := z + 2
Background on Compilers
Example : one more twist
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
x == 5 is NEVER possible under sequential consistency! (What is it ??)
Sequential Consistency (defined by Lamport)
https://en.wikipedia.org/wiki/Sequential_consistency
https://en.wikipedia.org/wiki/Leslie_Lamport
Example : one more twist
This program has a data race
Initially globals x == y == z == 0
P1 || P2
---------- ------------
y := 1 y := 2
x := z + 2
y := y + 1
z := y + x
Finally x == ?
x == 2 ? How ?
x == 3 ? How ?
x == 4 ? How ?
x == 5 is NEVER possible under sequential consistency!
Programmers (subconsciously ascribe the SC semantics to all concurrent programs)!
Summary
Data races can introduce behaviors outside of those formally specified for the program in question!
This may (for instance) variables reading values that were never written!
One more example
initially, globals x == 0, y == 0
(Let's use Hex)
P1 || P2 || P3
---------- ------------ -----------
x := DEAD x := BEEF y := x
Finally y == ?
y == DEAD how?
y == BEEF how?
y == DEEF how?
y == BEAD how?
One more example
initially, globals x == 0, y == 0
(Let's use Hex)
P1 || P2 || P3
---------- ------------ -----------
x := DEAD x := BEEF y := x
Finally y == ?
y == DEAD how?
y == BEEF how?
y == DEEF how? word tearing!
y == BEAD how? word tearing!
Hilarious example courtesy of Prof. John Regeher https://gcc.godbolt.org/z/dY4Pc1oxY
One more example
initially, globals x == 0, y == 0
(Let's use Hex)
P1 || P2 || P3
---------- ------------ -----------
x := DEAD x := BEEF y := x
Finally y == ?
y == DEAD how?
y == BEEF how?
y == DEEF how? word tearing!
y == BEAD how? word tearing!
Hilarious example courtesy of Prof. John Regeher https://gcc.godbolt.org/z/dY4Pc1oxY
One more example
initially, globals x == 0, y == 0
(Let's use Hex)
P1 || P2 || P3
---------- ------------ -----------
x := DEAD x := BEEF y := x
Finally y == ?
y == DEAD how?
y == BEEF how?
y == DEEF how? word tearing!
y == BEAD how? word tearing!
Hilarious example courtesy of Prof. John Regeher https://gcc.godbolt.org/z/dY4Pc1oxY
YET, we see abusive use of deprecated "volatile" in CUDA in the hopes of preventing tearing
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1152r0.html
One more example
initially, globals x == 0, y == 0
(Let's use Hex)
P1 || P2 || P3
---------- ------------ -----------
x := DEAD x := BEEF y := x
Finally y == ?
y == DEAD how?
y == BEEF how?
y == DEEF how? word tearing!
y == BEAD how? word tearing!
Hilarious example courtesy of Prof. John Regeher https://gcc.godbolt.org/z/dY4Pc1oxY
YET, we see abusive use of deprecated "C volatiles" in CUDA in the hopes of preventing tearing (see C-standards committee document that deprecates volatiles)
http://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p1152r0.html
Terminology Warning
Purpose of this lecture
Purpose of this lecture
Thus, all CUDA programs are suspect, and potentially broken!
(unless you can somehow check via manual reasoning…)
Organization
Overview: Input space of a program
Overview: Schedule-space of a program
Overview: You cannot exhaust input and schedule spaces
Before we do that, let's "see some races" that have arisen in the field
Races in OpenMP
Races in GPU Codes
Races in GPU Codes
(Background: 10-min Video - on Java Memory Models)
This video of 10 minutes
is done remarkably well!
In 10 minutes, it explains
Example of a non-racy Java program (see gist next slide)
Gist of a non-racy Java program easily made racy
(DEMO)
OR they are held in the cache and not flushed
Hard to debug (hard to even see the assembly code…)
Other Race Scenarios: affected by compiler optimizations
Other Race Scenarios: affected by compiler optimizations
Bugs Related to Races
Photoshop Bug
Photoshop Bug
To understand how to analyze programs, we need the notion of memory models
i.e. shared memory consistency models
not just memory organization models
Great examples from the JMM tutorial
There are HB edges from the assignments
to a,b,c and the write to x in writerThread
One can replace int r2 = x in readerThread()
with a while (x==0) { /* wait */ } loop
Then it is guaranteed that a,b,c will be 1 in
readerThread()
Great examples from the JMM tutorial
There are HB edges from the assignments
to a,b,c and the synchronized block in the writer
If x==1 in readerThread(), then
it guaranteed that a,b,c will be 1
Great examples from the JMM tutorial
Without the
volatile
declaration,
the readerThread()
need not exit
volatile inserts
fences
and also forces
stores
Gist of how dynamic race checkers check races
The importance of running sufficient # of interleavings
This slide also provides the only real portrayal of HB in some detail! Study it carefully!
Race Checking Concepts
Talk by Simone Atzeni
https://drive.google.com/drive/u/1/folders/16dqtgiRK-hjQnejWOEWJYM5NvSiWejk9
Race Examples from OMP
Slides by Simone Atzeni
https://drive.google.com/drive/u/1/folders/16dqtgiRK-hjQnejWOEWJYM5NvSiWejk9
Example of GPU (CUDA) Races
These slides present short GPU race scenarios and how our former GKLEE tool used to spot them
https://drive.google.com/drive/u/1/folders/1VMg3mWxxG1HsBeyroKpAXUoUVa9bPKPM
Example of Running Archer
Show demo using
docker pull tanmaytirpankar/openmpracechecker:1.0
and run Archer
(Class demo)
Race checking for PThreads, etc.
Many types of checks; see here (many are GCC / Clang flags)
https://github.com/google/sanitizers/wiki/
Most of these were created using the ideas in Flanagan's "FastTrack" which were made even more efficient by Google scientists Serebranyay and Vyukov
�These power Archer and Go's race checker as well
Our tool Sword uses a different approach
Static analysis based race checking of OMP : LLOV tool
Concluding Remarks