From d11b72cf08fec051dcd69cc920d1e6c0b6701407 Mon Sep 17 00:00:00 2001 From: Lennart Krauch Date: Tue, 2 Jul 2024 14:32:19 +0200 Subject: [PATCH] synced content from master Signed-off-by: Lennart Krauch --- .../content/docs/semesterplan/semSoSe24.md | 20 +- .../src/content/docs/teil_2/lec-deadlock.md | 684 ++++++++++++-- .../src/content/docs/teil_2/lec-hb-vc.md | 870 ++++++++++++++++-- .../src/content/docs/teil_2/lec-lockset.md | 622 +++++++++++-- 4 files changed, 1975 insertions(+), 221 deletions(-) diff --git a/astro-rewrite/src/content/docs/semesterplan/semSoSe24.md b/astro-rewrite/src/content/docs/semesterplan/semSoSe24.md index d9cebaa..3f3e529 100644 --- a/astro-rewrite/src/content/docs/semesterplan/semSoSe24.md +++ b/astro-rewrite/src/content/docs/semesterplan/semSoSe24.md @@ -81,23 +81,27 @@ Wöchentlicher Ablauf. - W8, 06.05-12.05 (Donnerstag Vorlesungsfrei) - Keine Vorlesung - W9, 13.05-19.05 - - Dynamische Data Race Erkennung - - Lockset Methode - - go-race + - Keine Vorlesung - Pfingstwoche Vorlesungsfrei, 20.05-26.05 - W10, 27.05-02.06 (Donnerstag Vorlesungsfrei) - Keine Vorlesung - W11, 03.06-09.06 - - Deadlock Analyse + - Dynamische Data Race Erkennung (Wiederholung) - W12, 10.06-16.06 + - Dynamische Data Race Erkennung + - Vector clocks + - FastTrack Algorithmus + - go-race +- W13, 17.06-23.06 + - Dynamische Data Race Erkennung + - Lockset Methode + - Deadlock Analyse +- W14, 24.06-30.06 - General purpose versus domain specific languages - Concurrency models (mutex, fork/join, barrier, wait/notify, futures) -- W13, 17.06-23.06 - - Concurrency models (more on futures) -- W14, 24.06-30.06 - - TBA - W15, 01.07-07.07 + - Concurrency models (more on futures) - Klausurinfo: - Schriftlich, ohne Hilfsmittel - Teil der Modulklausur Autonome Systeme + Rechner Architektur diff --git a/astro-rewrite/src/content/docs/teil_2/lec-deadlock.md b/astro-rewrite/src/content/docs/teil_2/lec-deadlock.md index 3d356e8..3303a77 100644 --- a/astro-rewrite/src/content/docs/teil_2/lec-deadlock.md +++ b/astro-rewrite/src/content/docs/teil_2/lec-deadlock.md @@ -243,75 +243,116 @@ are not in S2. ## Cycle check -We write *D* = (*i**d*, *l*, *l**s*) to refer to some lock dependency in -thread *i**d* where lock *l* is acquired while holding locks *l**s*. +We write `D = (id, l, ls)` to refer to some lock dependency in thread +`id` where lock `l` is acquired while holding locks *l**s*. A deadlock (warning) is issued if there is a cyclic lock dependency -chain *D*1, ..., *D**n*: +chain `D_1, ..., D_n` where each `D_i` results from a distinct thread +and the following conditions are met: -- (LD-1) *l**s**i* ∩ *l**s**j* = ⌀ for - *i*! = *j*, and +- (LD-1) `ls_i cap ls_j = {}` for `i != j`, and -- (LD-2) *l**i* ∈ *l**s**i* + 1 for - *i* = 1, ..., *n* − 1, and +- (LD-2) `l_i \in ls_i+1` for `i=1,...,n-1`, and -- (LD-3) *l**n* ∈ *l**s*1. +- (LD-3) `l_n \in ls_1`. -Note. Each *D**i* results from some distinct thread *i*. +Notation. + +`cap` stands for set intersection. +`S1 cap S2 = { x | x in S1 and x in S2 }`. + +`D_i` results from thread `i`. ## Examples -### Same thread +Traces are annotated with lock dependencies (generated via the “lock +dependency” implementation in the appendix). -Recall +### Standard example - T1 T2 LS_T1 LS_T2 + T0 T1 LockDep + e1. fork(T1) + e2. acq(L1) + e3. acq(L2) (T0,L2,{L1}) + e4. rel(L2) + e5. rel(L1) + e6. acq(L2) + e7. acq(L1) (T1,L1,{L2}) + e8. rel(L1) + e9. rel(L2) - 1. acq(y) {y} - 2. acq(x) {y,x} yields (T1,x,{y}) - 3. rel(x) {y} - 4. rel(y) {} - 5. acq(x) {x} - 6. acq(y) {x,y} yields (T1,y,{x}) - 7. rel(y) {x} - 8. rel(x) {} +`(T0,L2,{L1}), (T1,L1,{L2})` are in a cyclic lock dependency chain. -In summary, we find the following lock dependencies. +LD-1: {L1} cap {L2} = {} - (T1,x,{y}) - (T1,y,{x}) +LD-2: L2 in {L2} -No deadlock warning is issued because dependencies are from the same -thread T1. +LD-3: L1 in {L1} -### Guard lock +Indeed, there is a deadlock as shown by the following reordering. -Recall + T0 T1 LockDep + e1. fork(T1) + e2. acq(L1) + e6. acq(L2) - T1 T2 T1_LS T2_LS + We cannot extend the trace further because any of the next possible events that will follow are "blocked". + Recall that B-acq(L2) indicates that the acquire operation on L2 blocks. - 1. acq(z) z - 2. acq(y) z,y (T1,y,{z}) - 3. acq(x) z,y,x (T1,x,{y,z}) - 4. rel(x) z,y - 5. rel(y) z - 6. rel(z) - 7. acq(z) z - 8. acq(x) z,x (T2,x,{z}) - 9. acq(y) z,x,y (T2,y,{x,z}) - 10. rel(y) z,x - 11. rel(x) z - 12. rel(z) -For the above, we compute the following lock dependencies. + e7. B-acq(L1) + e3. B-acq(L2) + +By “blocked” we mean that by adding events e7 and e3 this will lead to +an invalid trace (because lock semantics is violated here). + +### Same thread + + T0 T1 LockDep + e1. fork(T1) + e2. acq(L1) + e3. rel(L1) + e4. acq(L1) + e5. acq(L2) (T0,L2,{L1}) + e6. rel(L2) + e7. rel(L1) + e8. acq(L2) + e9. acq(L1) (T0,L1,{L2}) + e10. rel(L1) + e11. rel(L2) + +`(T0,L2,{L1})` and `(T0,L1,{L2})` are not in a cyclic lock dependency +chain because they result from the same thread. + +### Guard lock + + T0 T1 LockDep + e1. fork(T1) + e2. acq(L3) + e3. acq(L1) (T0,L1,{L3}) + e4. acq(L2) (T0,L2,{L1,L3}) + e5. rel(L2) + e6. rel(L1) + e7. rel(L3) + e8. acq(L3) + e9. acq(L2) (T1,L2,{L3}) + e10. acq(L1) (T1,L1,{L3,L2}) + e11. rel(L1) + e12. rel(L2) + e13. rel(L3) + +In summary, we find the following lock dependencies. + + D1 = (T0,L1,{L3}) + D2 = (T0,L2,{L1,L3}) - D1 = (T1, y, {z}) - D2 = (T1, x, {y,z}) + D3 = (T1,L2,{L3}) + D4 = (T1,L1,{L3,L2}) - D3 = (T2, x, {z}) - D4 = (T2, y, {x,z}) +No deadlock warning is issued. -No deadlock warning is issued due to the common guard lock z. +For example, D2 and D3 are not in a cyclic lock dependency chain due to +the common guard lock `L3`. ## Precision (false positives and false negatives) @@ -322,67 +363,93 @@ positives and false negatives. Consider the following example. - T1 T2 - - 1. acq(y) - 2. acq(x) - 3. rel(x) - 4. rel(y) - 5. acq(z) - 6. wr(a) - 7. rel(z) - 8. acq(z) - 9. rd(a) - 10. rel(z) - 11. acq(x) - 12. acq(y) - 13. rel(y) - 14. rel(x) + T0 T1 LockDep + e1. fork(T1) + e2. acq(L1) + e3. acq(L2) (T0,L2,{L1}) + e4. rel(L2) + e5. rel(L1) + e6. acq(L3) + e7. wr(V1) + e8. rel(L3) + e9. acq(L3) + e10. rd(V1) + e11. rel(L3) + e12. acq(L2) + e13. acq(L1) (T1,L1,{L2}) + e14. rel(L1) + e15. rel(L2) We encounter the following lock dependencies. - D1 = (T1, x, {y}) + D1 = (T0,L2,{L1}) - D2 = (T2, y, {z}) + D2 = (T1,L1,{L2}) We issue a deadlock warning because D1, D2 form a cyclic lock dependency chain. This is false positive! Due to the write-read dependency, events in -thread T1 must happen before the events in thread T2. +thread T1 must happen before the events in thread T2. Hence, it is +impossible to find a reordering that results in a deadlock. + +Consider the following failed attempt. + + T0 T1 LockDep + e1. fork(T1) + e2. acq(L1) + e9. acq(L3) + e10. rd(V1) + e11. rel(L3) + e12. acq(L2) + +The above reordering is not valid. The read event e10 is missing its +“last write”. ## False negatives Consider the following example. - T1 T2 T3 - - 1. acq(x) - 2. fork(T2) - 3. acq(y) - 4. rel(y) - 5. join(T2) - 6. rel(x) - 7. acq(y) - 8. acq(x) - 9. rel(x) - 10. rel(y) + T0 T1 T2 LockDep + e1. fork(T2) + e2. acq(L1) + e3. fork(T1) + e4. acq(L2) + e5. rel(L2) + e6. join(T1) + e7. rel(L1) + e8. acq(L2) + e9. acq(L1) (T2,L1,{L2}) + e10. rel(L1) + e11. rel(L2) We compute the following dependency. - D1 = (T3,x,{y}) + D1 = (T2,L1,{L2}) + +As there is only a single lock dependency, no deadlock warning is +isused. -There appears to be no deadlock (no cycle) but there’s a trace -reordering under which we run into a deadlock. +However, we run into a deadlock situation as shown by the following +reordering. - T1 T2 T3 + T0 T1 T2 + e1. fork(T2) + e2. acq(L1) + e3. fork(T1) + e8. acq(L2) - 1. acq(x) - 2. fork(T2) - 7. acq(y) - 8. B-acq(x) - 3. B-acq(y) - 5. B-join(T2) + The events below are the "next" possible events to consider. + None of the events can be added to the trace cause this leads then to an invalid trace. + For example, events e4 and e9 violate lock semantics, event e6 violates the condition + that thread T1 is not fully completed. + + As before, we write B-join(T1), B-acq(L2) and B-acq(L1) to indicate that these events + are "blocked" and cannot be added to the trace. + + e9. B-acq(L1) + e4. B-acq(L2) + e6. B-join(T1) The above is an example of a *cross-thread* critical section that includes several events due to the fork/join dependency. However, the @@ -494,12 +561,453 @@ TSan reports a deadlock but this is a clear false positive. - False positives and false negatives remain an issue. + - False positive means that there exists a cyclic lock dependency + chain but there is no valid reordering that results in a + deadlock. + + - False negative means that there is a reordering that results in + a deadlock but there is no cyclic lock dependency chain. + - Go-style mutexes pose further challenges (false positives). - On-going research to reduce the amount of false positives and false negatives. -## Appendix: Some implementation in Go +## Appendix: Some implementations in Go + +Lock dependencies + +[Go playground](https://go.dev/play/p/PpZNexJfw-t) + + package main + + // Deadlock detection based on lock dependencies + + import "fmt" + import "strconv" + import "strings" + + // Example traces. + + // Traces are assumed to be well-formed. + // For example, if we fork(ti) we assume that thread ti exists. + + // Standard example + func trace_1() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + y := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + acq(t0, y), + rel(t0, y), + rel(t0, x), + acq(t1, y), + acq(t1, x), + rel(t1, x), + rel(t1, y)} + + } + + // Same Thread + func trace_2() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + y := 2 + return []Event{ + fork(t0, t1), + acq(t1, x), + rel(t1, x), + acq(t0, x), + acq(t0, y), + rel(t0, y), + rel(t0, x), + acq(t0, y), + acq(t0, x), + rel(t0, x), + rel(t0, y)} + + } + + // Guard lock + func trace_3() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + y := 2 + z := 3 + return []Event{ + fork(t0, t1), + acq(t0, z), + acq(t0, x), + acq(t0, y), + rel(t0, y), + rel(t0, x), + rel(t0, z), + acq(t1, z), + acq(t1, y), + acq(t1, x), + rel(t1, x), + rel(t1, y), + rel(t1, z)} + + } + + // False positive due to write-read dependency + func trace_4() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + y := 2 + z := 3 + a := 1 + return []Event{ + fork(t0, t1), + acq(t0, x), + acq(t0, y), + rel(t0, y), + rel(t0, x), + acq(t0, z), + wr(t0, a), + rel(t0, z), + acq(t1, z), + rd(t1, a), + rel(t1, z), + acq(t1, y), + acq(t1, x), + rel(t1, x), + rel(t1, y)} + + } + + func trace_5() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + x := 1 + y := 2 + return []Event{ + fork(t0, t2), + acq(t0, x), + fork(t0, t1), + acq(t1, y), + rel(t1, y), + join(t0, t1), + rel(t0, x), + acq(t2, y), + acq(t2, x), + rel(t2, x), + rel(t2, y)} + + } + + func main() { + + run(trace_1()) + + run(trace_2()) + + run(trace_3()) + + run(trace_4()) + + run(trace_5()) + + } + + /////////////////////////////////////////////////////////////// + // Helpers + + func max(x, y int) int { + if x < y { + return y + } + return x + } + + func debug(s string) { + fmt.Printf("%s", s) + + } + + /////////////////////////////////////////////////////////////// + // Events + + type EvtKind int + + const ( + AcquireEvt EvtKind = 0 + ReleaseEvt EvtKind = 1 + WriteEvt EvtKind = 2 + ReadEvt EvtKind = 3 + ForkEvt EvtKind = 4 + JoinEvt EvtKind = 5 + ) + + type Event struct { + k_ EvtKind + id_ int + a_ int + } + + func (e Event) thread() int { return e.id_ } + func (e Event) kind() EvtKind { return e.k_ } + func (e Event) arg() int { return e.a_ } + + // Some convenience functions. + func rd(i int, a int) Event { + return Event{ReadEvt, i, a} + } + + func wr(i int, a int) Event { + return Event{WriteEvt, i, a} + } + + func acq(i int, a int) Event { + return Event{AcquireEvt, i, a} + } + + func rel(i int, a int) Event { + return Event{ReleaseEvt, i, a} + } + + func fork(i int, a int) Event { + return Event{ForkEvt, i, a} + } + + func join(i int, a int) Event { + return Event{JoinEvt, i, a} + } + + // Trace assumptions. + // Initial thread starts with 0. Threads have ids in ascending order. + + func trace_info(es []Event) (int, map[int]bool, map[int]bool) { + max_tid := 0 + vars := map[int]bool{} + locks := map[int]bool{} + for _, e := range es { + max_tid = max(max_tid, e.thread()) + if e.kind() == WriteEvt || e.kind() == ReadEvt { + vars[e.arg()] = true + } + if e.kind() == AcquireEvt { // For each rel(x) there must exists some acq(x) + locks[e.arg()] = true + } + } + return max_tid, vars, locks + } + + func mainThread() int { return 0 } + func nextThread(i int) int { return i + 1 } + + const ( + ROW_OFFSET = 14 + ) + + // Omit thread + loc info. + func displayEvtSimple(e Event) string { + var s string + arg := strconv.Itoa(e.arg()) + switch { + case e.kind() == AcquireEvt: + s = "acq(L" + arg + ")" // L(ock) + case e.kind() == ReleaseEvt: + s = "rel(L" + arg + ")" + case e.kind() == WriteEvt: + s = "wr(V" + arg + ")" // V(ar) + case e.kind() == ReadEvt: + s = "rd(V" + arg + ")" + case e.kind() == ForkEvt: + s = "fork(T" + arg + ")" // T(hread) + case e.kind() == JoinEvt: + s = "join(T" + arg + ")" + } + return s + } + + func colOffset(i int, row_offset int) string { + n := (int)(i) + return strings.Repeat(" ", n*row_offset) + } + + // Thread ids fully cover [0..n] + func displayTraceWithLockDep(m int, es []Event, evt_ld map[int]LockDep, row_offset int) string { + s := "" + for i, e := range es { + ld_info := " " + trace_position := i + 1 // trace position starts with 1 + _, ok := evt_ld[trace_position] + if ok { + ld_info += evt_ld[trace_position].display() + } + row := "\n" + "e" + strconv.Itoa(i+1) + ". " + colOffset(e.thread(), row_offset) + displayEvtSimple(e) + colOffset(m-e.thread(), row_offset) + ld_info + s = s + row + } + // Add column headings. + heading := " " + for i := 0; i <= m; i++ { + heading += "T" + strconv.Itoa(i) + strings.Repeat(" ", row_offset-2) + } + heading += "LockDep" + s = heading + s + + return s + } + + /////////////////////////////////////////////////////////////// + // Lock sets + lock depenencies + + type LS map[int]bool + + type LockDep struct { + thread_id int + lock int + ls LS + } + + func (ls LS) empty() bool { + return len(ls) == 0 + + } + + func (ls LS) add(x int) { + ls[x] = true + } + + func (ls LS) remove(x int) { + delete(ls, x) + } + + func (ls LS) display() string { + var s string + i := len(ls) + s = "{" + for lock, _ := range ls { + + if i > 1 { + s = s + "L" + strconv.Itoa(lock) + "," + + } + if i == 1 { + s = s + "L" + strconv.Itoa(lock) + } + i-- + } + return s + "}" + } + + func (ld LockDep) display() string { + var s string + s = "(T" + strconv.Itoa(ld.thread_id) + ",L" + strconv.Itoa(ld.lock) + "," + ld.ls.display() + ")" + + return s + + } + + func copyLS(ls LS) LS { + new := make(map[int]bool) + for lock, _ := range ls { + new[lock] = true + } + + return new + } + + /////////////////////////////////////////////////////////////// + + type State struct { + th_lockset map[int]LS // key = thread id + evt_lock_dep map[int]LockDep // key = trace position + trace_position int + } + + func run(es []Event) { + + var s State + + s.th_lockset = make(map[int]LS) + s.evt_lock_dep = make(map[int]LockDep) + s.trace_position = 1 + + max_tid := 0 + + for _, e := range es { + max_tid = max(max_tid, e.thread()) + } + + for i := 0; i <= max_tid; i++ { + s.th_lockset[i] = make(map[int]bool) + } + + exec := func(e Event) { + switch { + case e.kind() == AcquireEvt: + s.acquire(e) + case e.kind() == ReleaseEvt: + s.release(e) + case e.kind() == ForkEvt: + s.fork(e) + case e.kind() == JoinEvt: + s.join(e) + case e.kind() == WriteEvt: + s.write(e) + case e.kind() == ReadEvt: + s.read(e) + } + + } + + for _, e := range es { + exec(e) + s.trace_position = s.trace_position + 1 + + } + + fmt.Printf("\n%s\n", displayTraceWithLockDep(max_tid, es, s.evt_lock_dep, 12)) + + } + + func (s *State) acquire(e Event) { + t := e.thread() + y := e.arg() + + if !s.th_lockset[t].empty() { + ld := LockDep{t, y, copyLS(s.th_lockset[t])} + s.evt_lock_dep[s.trace_position] = ld + + } + + s.th_lockset[t].add(y) + + } + + func (s *State) release(e Event) { + t := e.thread() + y := e.arg() + s.th_lockset[t].remove(y) + } + + func (s *State) fork(e Event) { + + } + + func (s *State) join(e Event) { + + } + + func (s *State) write(e Event) { + + } + + func (s *State) read(e Event) { + + } + +## Appendix: Lock graph Here comes a simple implementation for dynamic deadlock prediction based on lock graphs. diff --git a/astro-rewrite/src/content/docs/teil_2/lec-hb-vc.md b/astro-rewrite/src/content/docs/teil_2/lec-hb-vc.md index 9859b37..317a63b 100644 --- a/astro-rewrite/src/content/docs/teil_2/lec-hb-vc.md +++ b/astro-rewrite/src/content/docs/teil_2/lec-hb-vc.md @@ -218,6 +218,9 @@ where *i*! = *j* and *n* > 0. Then, we find that Hence, the critical section order only needs to consider a release and a later in trace appearing acquire. +*The HB relation does not enforce the last writer rule. More on this +later.* + ## Example Consider the trace @@ -634,7 +637,7 @@ We define < and *s**y**n**c* for vector clocks as follows. Order among vector clocks - [i1,...,in] < [j1,...,jn]) + [i1,...,in] < [j1,...,jn] if ik<=jk for all k=1...n and there exists k such that ik Th(t)(j) then write in a race with a write - then write-write race (W(x),e) W(x) = t##Th(t)(t) inc(Th(t),t) @@ -719,81 +721,815 @@ Event processing. if k > Th(t)(j) then read in a race with a write R(x) = sync(Th(t), R(x)) + inc(Th(t),t) } -We follow Java’s memory semantics. +Points note note. -We impose last-write order only for atomic variables. +We include `fork` and `join` events. -Atomic variables are protected by a lock. As we order critical sections -based on their textual occurrence, we get the last-write order for -atomic variables for free. +FastTrack (like the HB relation) does not enforce the “last writer” +rule. This is in line with We Java’s “weak” memory semantics. -We include `fork` and `join` events. +The last-write order is enforced for atomic variables. Atomic variables +are protected by a lock. As we order critical sections based on their +textual occurrence, we get the last-write order for atomic variables for +free. -## Examples (from before) +## FastTrack Examples (from before) -### Race not detected +The following examples are automatically generated. There is a slight +change in naming convention. Instead of lock variable “x” we write “L1”. +Similarly, we write “V0” for some shared variable “y”. - T0 T1 +## Race not detected - 1. fork(T1) [1,0] - 2. acq(x) [2,0] - 3. wr(z) [3,0] W(z) = undefined - 4. rel(x) [4,0] - 5. acq(x) [1,1] - 6. rel(x) [4,2] - 7. wr(z) [4,3] W(z) = 0##3 +Consider the following trace. -- For each event we annotate its vector clock + T0 T1 + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) + e4. rel(L1) + e5. acq(L1) + e6. rel(L1) + e7. wr(V2) + +We apply the FastTrack algorithm on the above trace. For each event we +annotate its vector clock before and after processing the event. + + T0 T1 + e1. [1,0]_fork(T1)_[2,0] + e2. [2,0]_acq(L1)_[3,0] + e3. [3,0]_wr(V2)_[4,0] + e4. [4,0]_rel(L1)_[5,0] + e5. [1,1]_acq(L1)_[4,2] + e6. [4,2]_rel(L1)_[4,3] + e7. [4,3]_wr(V2)_[4,4] + +Here are the individual processing steps in detail. + + **** + Step 1: Processing event fork(T1)in thread T0 + BEFORE + Thread VC = [1,0] + AFTER + Thread VC = [2,0] + **** + Step 2: Processing event acq(L1)in thread T0 + BEFORE + Thread VC = [2,0] + Rel[L1] = [0,0] + AFTER + Thread VC = [3,0] + Rel[L1] = [0,0] + **** + Step 3: Processing event wr(V2)in thread T0 + BEFORE + Thread VC = [3,0] + R[V2] = [0,0] + W[V2] = undefined + AFTER + Thread VC = [4,0] + R[V2] = [0,0] + W[V2] = 0##3 + **** + Step 4: Processing event rel(L1)in thread T0 + BEFORE + Thread VC = [4,0] + Rel[L1] = [0,0] + AFTER + Thread VC = [5,0] + Rel[L1] = [4,0] + **** + Step 5: Processing event acq(L1)in thread T1 + BEFORE + Thread VC = [1,1] + Rel[L1] = [4,0] + AFTER + Thread VC = [4,2] + Rel[L1] = [4,0] + **** + Step 6: Processing event rel(L1)in thread T1 + BEFORE + Thread VC = [4,2] + Rel[L1] = [4,0] + AFTER + Thread VC = [4,3] + Rel[L1] = [4,2] + **** + Step 7: Processing event wr(V2)in thread T1 + BEFORE + Thread VC = [4,3] + R[V2] = [0,0] + W[V2] = 0##3 + AFTER + Thread VC = [4,4] + R[V2] = [0,0] + W[V2] = 1##3 + +## Race detected -- For each write we show the state of W(x) before processing the read + T0 T1 + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) + e4. rel(L1) + e5. wr(V2) + e6. acq(L1) + e7. rel(L1) + +In case of a race detected, we annotate the triggering event. + + T0 T1 + e1. [1,0]_fork(T1)_[2,0] + e2. [2,0]_acq(L1)_[3,0] + e3. [3,0]_wr(V2)_[4,0] + e4. [4,0]_rel(L1)_[5,0] + e5. [1,1]_wr(V2)_[1,2] WW + e6. [1,2]_acq(L1)_[4,3] + e7. [4,3]_rel(L1)_[4,4] + +The annotation `WW` indicates that write event `e4` is in a race with +some earlier write. + +For brevity, we omit the detailed processing steps. -- If there are any reads we also show R(x) +### Earlier race not detected -### Race detected + T0 T1 + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) + e4. wr(V2) + e5. rel(L1) + e6. wr(V2) + e7. acq(L1) + e8. rel(L1) + +Event `e6` is in a race with `e4` and `e3`. However, FastTrack only +maintains the “last” write. Hence, FastTrack only reports the race among +`e6` and `e4`. + +Here is the annotated trace. + + T0 T1 + e1. [1,0]_fork(T1)_[2,0] + e2. [2,0]_acq(L1)_[3,0] + e3. [4,0]_wr(V2)_[5,0] + e4. [4,0]_wr(V2)_[5,0] + e5. [5,0]_rel(L1)_[6,0] + e6. [1,1]_wr(V2)_[1,2] WW + e7. [1,2]_acq(L1)_[5,3] + e8. [5,3]_rel(L1)_[5,4] - T0 T1 +### Read-write races - 1. fork(T1) [1,0] - 2. acq(x) [2,0] - 3. wr(z) [3,0] W(z) = undefined - 4. rel(x) [4,0] - 5. wr(z) [1,1] W(z) = 0##3 - 6. acq(x) [1,2] - 7. rel(x) [4,3] +The following trace contains reads as well as writes. -### Earlier race not detected + T0 T1 T2 + e1. wr(V2) + e2. fork(T1) + e3. fork(T2) + e4. rd(V2) + e5. rd(V2) + e6. acq(L1) + e7. wr(V2) + e8. rel(L1) - T0 T1 +FastTrack reports that the write `e7` is in a race with a read. See the +annotation `RW` below. - 1. fork(T1) [1,0] - 2. acq(y) [2,0] - 3. wr(x) [3,0] W(x) = undefined - 4. wr(x) [4,0] W(x) = 0##3 - 5. rel(y) [5,0] - 6. wr(x) [1,1] W(x) = 0##4 - 7. acq(y) [1,2] - 8. rel(y) [5,3] + T0 T1 T2 + e1. [1,0,0]_wr(V2)_[2,0,0] + e2. [2,0,0]_fork(T1)_[3,0,0] + e3. [3,0,0]_fork(T2)_[4,0,0] + e4. [4,0,0]_rd(V2)_[5,0,0] + e5. [2,1,0]_rd(V2)_[2,2,0] + e6. [3,0,1]_acq(L1)_[3,0,2] + e7. [3,0,2]_wr(V2)_[3,0,3] RW + e8. [3,0,3]_rel(L1)_[3,0,4] -### Read-write races +There are two read-write races: (`e4`,`e7`) and (`e5`,`e7`). In our +FastTrack implementation, we only report the triggering event. - T0 T1 T2 +Here is a variant of the above example where we find write-write and +write-read and read-write races. + + T0 T1 T2 + e1. fork(T1) + e2. fork(T2) + e3. wr(V2) + e4. rd(V2) + e5. rd(V2) + e6. acq(L1) + e7. wr(V2) + e8. rel(L1) + +Here is the annotated trace. + + T0 T1 T2 + e1. [1,0,0]_fork(T1)_[2,0,0] + e2. [2,0,0]_fork(T2)_[3,0,0] + e3. [3,0,0]_wr(V2)_[4,0,0] + e4. [4,0,0]_rd(V2)_[5,0,0] + e5. [1,1,0]_rd(V2)_[1,2,0] WR + e6. [2,0,1]_acq(L1)_[2,0,2] + e7. [2,0,2]_wr(V2)_[2,0,3] RW WW + e8. [2,0,3]_rel(L1)_[2,0,4] + +## FastTrack Implementation in Go + +[Go playground](https://go.dev/play/p/FJb7BDk6Tyl) + +Check out main and the examples. + + package main + + // FastTrack + + import "fmt" + import "strconv" + import "strings" - 1. wr(x) [1,0,0] W(x) = undefined - 2. fork(T1) [2,0,0] - 3. fork(T2) [3,0,0] - 4. rd(x) [4,0,0] - 5. rd(x) [2,1,0] - 6. acq(y) [3,0,1] - 7. wr(x) [3,0,2] W(x) = 0##1 R(x) = [0##4,1##1] - 8. rel(y) [3,0,3] + + + // Example traces. + + // Traces are assumed to be well-formed. + // For example, if we fork(ti) we assume that thread ti exists. + + // Race not detected + func trace_1() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + rel(t0, x), + acq(t1, x), + rel(t1, x), + wr(t1, z)} + } + + // Race detected + func trace_2() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + rel(t0, x), + wr(t1, z), + acq(t1, x), + rel(t1, x)} + + } + + // Earlier race not detected + func trace_2b() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + wr(t0, z), + rel(t0, x), + wr(t1, z), + acq(t1, x), + rel(t1, x)} + + } + + // Read-write races + func trace_3() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + x := 1 + z := 2 + return []Event{ + wr(t0, z), + fork(t0, t1), + fork(t0, t2), + rd(t0, z), + rd(t1, z), + acq(t2, x), + wr(t2, z), + rel(t2, x)} + + } + + // Write-write and wwrite-read and read-write races + func trace_3b() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + fork(t0, t2), + wr(t0, z), + rd(t0, z), + rd(t1, z), + acq(t2, x), + wr(t2, z), + rel(t2, x)} + + } + + func main() { + + // fmt.Printf("\n%s\n", displayTrace(trace_1())) + // run(trace_1(), true) + + // fmt.Printf("\n%s\n", displayTrace(trace_2())) + // run(trace_2(), true) + + // fmt.Printf("\n%s\n", displayTrace(trace_2b())) + // run(trace_2b(), true) + + // fmt.Printf("\n%s\n", displayTrace(trace_3())) + // run(trace_3(), true) + + // fmt.Printf("\n%s\n", displayTrace(trace_3b())) + // run(trace_3b(), true) + + } + + + + + /////////////////////////////////////////////////////////////// + // Helpers + + func max(x, y int) int { + if x < y { + return y + } + return x + } + + func debug(s string) { + fmt.Printf("%s", s) + + } + + /////////////////////////////////////////////////////////////// + // Events + + type EvtKind int + + const ( + AcquireEvt EvtKind = 0 + ReleaseEvt EvtKind = 1 + WriteEvt EvtKind = 2 + ReadEvt EvtKind = 3 + ForkEvt EvtKind = 4 + JoinEvt EvtKind = 5 + ) + + type Event struct { + k_ EvtKind + id_ int + a_ int + } + + func (e Event) thread() int { return e.id_ } + func (e Event) kind() EvtKind { return e.k_ } + func (e Event) arg() int { return e.a_ } + + // Some convenience functions. + func rd(i int, a int) Event { + return Event{ReadEvt, i, a} + } + + func wr(i int, a int) Event { + return Event{WriteEvt, i, a} + } + + func acq(i int, a int) Event { + return Event{AcquireEvt, i, a} + } + + func rel(i int, a int) Event { + return Event{ReleaseEvt, i, a} + } + + func fork(i int, a int) Event { + return Event{ForkEvt, i, a} + } + + func join(i int, a int) Event { + return Event{JoinEvt, i, a} + } + + // Trace assumptions. + // Initial thread starts with 0. Threads have ids in ascending order. + + func trace_info(es []Event) (int, map[int]bool, map[int]bool) { + max_tid := 0 + vars := map[int]bool{} + locks := map[int]bool{} + for _, e := range es { + max_tid = max(max_tid, e.thread()) + if e.kind() == WriteEvt || e.kind() == ReadEvt { + vars[e.arg()] = true + } + if e.kind() == AcquireEvt { // For each rel(x) there must exists some acq(x) + locks[e.arg()] = true + } + } + return max_tid, vars, locks + } + + func mainThread() int { return 0 } + func nextThread(i int) int { return i + 1 } + + const ( + ROW_OFFSET = 14 + ) + + // Omit thread + loc info. + func displayEvtSimple(e Event, i int) string { + var s string + arg := strconv.Itoa(e.arg()) + switch { + case e.kind() == AcquireEvt: + s = "acq(L" + arg + ")" // L(ock) + case e.kind() == ReleaseEvt: + s = "rel(L" + arg + ")" + case e.kind() == WriteEvt: + s = "wr(V" + arg + ")" // V(ar) + case e.kind() == ReadEvt: + s = "rd(V" + arg + ")" + case e.kind() == ForkEvt: + s = "fork(T" + arg + ")" // T(hread) + case e.kind() == JoinEvt: + s = "join(T" + arg + ")" + } + return s + } + + func colOffset(i int, row_offset int) string { + n := (int)(i) + return strings.Repeat(" ", n*row_offset) + } + + // Thread ids fully cover [0..n] + func displayTraceHelper(es []Event, row_offset int, displayEvt func(e Event, i int) string) string { + s := "" + m := 0 + for i, e := range es { + row := "\n" + "e" + strconv.Itoa(i+1) + ". " + colOffset(e.thread(), row_offset) + displayEvt(e, i) + s = s + row + m = max(m, e.thread()) + } + // Add column headings. + heading := " " + for i := 0; i <= m; i++ { + heading += "T" + strconv.Itoa(i) + strings.Repeat(" ", row_offset-2) + } + s = heading + s + + return s + } + + func displayTrace(es []Event) string { + return displayTraceHelper(es, ROW_OFFSET, displayEvtSimple) + } + + func displayTraceWithVC(es []Event, pre map[Event]VC, post map[Event]VC, races map[Event]string) string { + displayEvt := func(e Event, i int) string { + out := pre[e].display() + "_" + displayEvtSimple(e, i) + "_" + post[e].display() + info, exists := races[e] + if exists { + out = out + " " + info + + } + return out + + } + return displayTraceHelper(es, 30, displayEvt) + } + + /////////////////////////////////////////////////////////////// + // Vector Clocks + + type VC []int + + type Epoch struct { + tid int + time_stamp int + } + + func (e Epoch) display() string { + return strconv.Itoa(e.tid) + "##" + strconv.Itoa(e.time_stamp) + + } + + func (v VC) display() string { + var s string + s = "[" + for index := 0; index < len(v)-1; index++ { + s = s + strconv.Itoa(v[index]) + "," + + } + if len(v) > 0 { + s = s + strconv.Itoa(v[len(v)-1]) + "]" + } + return s + + } + + func copyVC(v VC) VC { + new := make(VC, len(v)) + copy(new, v) + return new + } + + func sync(v VC, v2 VC) VC { + l := max(len(v), len(v2)) + + v3 := make([]int, l) + + for tid, _ := range v3 { + + v3[tid] = max(v[tid], v2[tid]) + } + + return v3 + } + + func (v VC) happensBefore(v2 VC) bool { + b := false + for tid := 0; tid < max(len(v), len(v2)); tid++ { + if v[tid] > v2[tid] { + return false + } else if v[tid] < v2[tid] { + b = true + } + + } + return b + } + + func (e Epoch) happensBefore(v VC) bool { + return e.time_stamp <= v[e.tid] + + } + + /////////////////////////////////////////////////////////////// + // Vector Clocks + + type FT struct { + Th map[int]VC + pre map[Event]VC + post map[Event]VC + Rel map[int]VC + W map[int]Epoch + R map[int]VC + races map[Event]string + i int + } + + func run(es []Event, full_info bool) { + + var ft FT + + ft.Th = make(map[int]VC) + ft.pre = make(map[Event]VC) + ft.post = make(map[Event]VC) + ft.Rel = make(map[int]VC) + ft.W = make(map[int]Epoch) + ft.R = make(map[int]VC) + ft.races = make(map[Event]string) + + n, vars, locks := trace_info(es) + n = n + 1 + + // Initial vector clock of T0 + ft.Th[0] = make([]int, n) + for j := 0; j < n; j++ { + ft.Th[0][j] = 0 + } + ft.Th[0][0] = 1 + + for x, _ := range vars { + ft.R[x] = make([]int, n) // all entries are zero + } + + for y, _ := range locks { + ft.Rel[y] = make([]int, n) // all entries are zero + } + + exec := func(e Event) { + switch { + case e.kind() == AcquireEvt: + ft.acquire(e) + case e.kind() == ReleaseEvt: + ft.release(e) + case e.kind() == ForkEvt: + ft.fork(e) + case e.kind() == JoinEvt: + ft.join(e) + case e.kind() == WriteEvt: + ft.write(e) + case e.kind() == ReadEvt: + ft.read(e) + } + + } + + infoBefore := func(i int, e Event) { + + if full_info { + + x := strconv.Itoa(e.arg()) + + out := "\n****\nStep " + strconv.Itoa(i) + ": Processing event " + displayEvtSimple(e, i) + "in thread T" + strconv.Itoa(e.thread()) + out = out + "\nBEFORE" + out = out + "\nThread VC = " + ft.Th[e.thread()].display() + + if e.kind() == AcquireEvt || e.kind() == ReleaseEvt { + out = out + "\nRel[L" + x + "] = " + ft.Rel[e.arg()].display() + + } + + if e.kind() == WriteEvt || e.kind() == ReadEvt { + out = out + "\nR[V" + x + "] = " + ft.R[e.arg()].display() + + ep, exists := ft.W[e.arg()] + if exists { + out = out + "\nW[V" + x + "] = " + ep.display() + } else { + out = out + "\nW[V" + x + "] = undefined" + } + + } + + fmt.Printf("%s", out) + } + + } + + infoAfter := func(e Event) { + + if full_info { + + x := strconv.Itoa(e.arg()) + + out := "\nAFTER" + out = out + "\nThread VC = " + ft.Th[e.thread()].display() + + if e.kind() == AcquireEvt || e.kind() == ReleaseEvt { + out = out + "\nRel[L" + x + "] = " + ft.Rel[e.arg()].display() + + } + + if e.kind() == WriteEvt || e.kind() == ReadEvt { + out = out + "\nR[V" + x + "] = " + ft.R[e.arg()].display() + + ep, exists := ft.W[e.arg()] + if exists { + out = out + "\nW[V" + x + "] = " + ep.display() + } else { + out = out + "\nW[V" + x + "] = undefined" + } + + } + + fmt.Printf("%s", out) + } + + } + + for i, e := range es { + infoBefore(i+1, e) + ft.pre[e] = copyVC(ft.Th[e.thread()]) + exec(e) + infoAfter(e) + ft.post[e] = copyVC(ft.Th[e.thread()]) + } + + fmt.Printf("\n%s\n", displayTraceWithVC(es, ft.pre, ft.post, ft.races)) + + } + + // We only report the event that triggered the race. + func (ft *FT) logWR(e Event) { + ft.races[e] = "WR" // "write-read race" + } + + // A write might be in a race with a write and a read, so must add any race message. + func (ft *FT) logRW(e Event) { + _, exists := ft.races[e] + if !exists { + ft.races[e] = "" + } + ft.races[e] = ft.races[e] + " " + "RW" // "read-write race" + + } + + func (ft *FT) logWW(e Event) { + _, exists := ft.races[e] + if !exists { + ft.races[e] = "" + } + ft.races[e] = ft.races[e] + " " + "WW" // "write-write race" + } + + func (ft *FT) inc(t int) { + ft.Th[t][t] = ft.Th[t][t] + 1 + + } + + func (ft *FT) acquire(e Event) { + t := e.thread() + y := e.arg() + vc, ok := ft.Rel[y] + if ok { + ft.Th[t] = sync(ft.Th[t], vc) + } + ft.inc(t) + + } + + func (ft *FT) release(e Event) { + t := e.thread() + y := e.arg() + ft.Rel[y] = copyVC(ft.Th[t]) + ft.inc(t) + } + + func (ft *FT) fork(e Event) { + t1 := e.thread() + t2 := e.arg() + ft.Th[t2] = copyVC(ft.Th[t1]) + ft.inc(t1) + ft.inc(t2) + } + + func (ft *FT) join(e Event) { + t1 := e.thread() + t2 := e.arg() + ft.Th[t1] = sync(ft.Th[t1], ft.Th[t2]) + ft.inc(t1) + + } + + func (ft *FT) write(e Event) { + t := e.thread() + x := e.arg() + + if !ft.R[x].happensBefore(ft.Th[t]) { + ft.logRW(e) + } + + ep, exists := ft.W[x] + if exists { + if !ep.happensBefore(ft.Th[t]) { + ft.logWW(e) + } + + } + + ft.W[x] = Epoch{tid: t, time_stamp: ft.Th[t][t]} + ft.inc(t) + + } + + func (ft *FT) read(e Event) { + t := e.thread() + x := e.arg() + ep, exists := ft.W[x] + if exists { + if !ep.happensBefore(ft.Th[t]) { + ft.logWR(e) + } + + ft.R[x] = sync(ft.Th[t], ft.R[x]) + + } + ft.inc(t) + + } ## Summary ## False negatives -The HB method as *false negatives*. This is due to the fact that the +The HB method has *false negatives*. This is due to the fact that the textual order among critical sections is preserved. Consider the following trace. @@ -917,8 +1653,7 @@ positions. 2. w(y) In the reordered trace II, the two writes on x appear right next to each -other. Is there a program run and that yields the above reordered trace? -No! +other. Is there a program run that yields the above reordered trace? No! In the reordered trace II, we violate the write-read dependency between *w*(*y*)2 and *r*(*y*)3. *w*(*y*)2 is @@ -959,6 +1694,33 @@ READ. However, the read value does not influence the control flow. Hence, for the above program trace II would be a valid reordering of trace I. +### Weak memory models + +There are further reasons why we can argue that there is no false +positive. Consider the original trace. + + Trace I: + + T1 T2 + + 1. w(x) + 2. w(y) + 3. r(y) + 4. w(x) + +The HB relation applies the program order condition. If we consider a +specific thread, then events are executed one after the other. + +On today’s modern computer architecture such rules no longer apply. We +may execute events “out of order” if they do not interfere. + +For example, we can argume that the read event `r(y)` and the write +event `w(x)` in thread T2 do not interfere with each other (as they +operate on distinct variables). Hence, we may process `w(x)` before +`r(y)`! There are also compiler optimizations where we speculatively +execute `w(x)` before `r(y)`. Hence, we can argue that the data race +among the writes on x is not a false positive. + ## Further reading ### [What Happens-After the First Race?](https://arxiv.org/pdf/1808.00185.pdf) diff --git a/astro-rewrite/src/content/docs/teil_2/lec-lockset.md b/astro-rewrite/src/content/docs/teil_2/lec-lockset.md index dc8243c..85859d4 100644 --- a/astro-rewrite/src/content/docs/teil_2/lec-lockset.md +++ b/astro-rewrite/src/content/docs/teil_2/lec-lockset.md @@ -258,101 +258,581 @@ we again find that *L**S*(*e*1) = {} and *L**S*(*e*5) = {*y*}. ## Further examples -We annotate the trace with lockset information. +The following examples are automatically generated. Traces are annotated +with lockset information (for reads/writes only). ## Example 1 - T0 T1 Lockset - 1. acq(y) - 2. w(x) {y} - 3. rel(y) - 4. r(x) {} - 5. w(x) {} - 6. acq(y) - 7. rel(y) + T0 T1 Lockset + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) {L1} + e4. rel(L1) + e5. acq(L1) + e6. rel(L1) + e7. wr(V2) {} -Lockset of the two writes on `x` in thread T0 and T1 are disjont. Hence, -the lockset method reports that there’s a data race. +Locksets of the writes are disjoint. Hence, we issue a data race +warning. This is a true positive. ## Example 2 - T0 T1 Lockset - 1. w(x) {} - 2. acq(y) - 3. w(x) {y} - 4. rel(y) - 5. acq(y) - 6. w(x) {y} - 7. rel(y) + T0 T1 Lockset + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) {L1} + e4. rel(L1) + e5. wr(V2) {} + e6. acq(L1) + e7. rel(L1) + +Locksets of the writes are disjoint. Hence, we issue a data race +warning. This is a true positive. + +## Example 2b + + T0 T1 Lockset + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) {L1} + e4. wr(V2) {L1} + e5. rel(L1) + e6. wr(V2) {} + e7. acq(L1) + e8. rel(L1) + +Each write in thread T0 is in a race with the write in thread T1 +(because their locksets are disjoint). -The lockset of the write at trace position 1 and the write at trace -position 6 are disjoint. Hence, we expect that the lockset method -signals that there is a data race. +## Example 3 -To be efficient, implemementation based on the lockset method only keep -track of the most recent locksets. That is, each thread maintains a list -of the most recent reads/writes plus their locksets. + T0 T1 T2 Lockset + e1. wr(V2) {} + e2. fork(T1) + e3. fork(T2) + e4. rd(V2) {} + e5. rd(V2) {} + e6. acq(L1) + e7. wr(V2) {L1} + e8. rel(L1) + +Each read (in thread T0 and thread T1) is in a race with the write in +thread T2 (because their locksets are disjoint). + +## Example 3b + + T0 T1 T2 Lockset + e1. fork(T1) + e2. fork(T2) + e3. wr(V2) {} + e4. rd(V2) {} + e5. rd(V2) {} + e6. acq(L1) + e7. wr(V2) {L1} + e8. rel(L1) + +The locksets of the write and read in thread T0 are disjoint. This is +not a race because the write and read take place in the same thread. +Recall that we only consider pairs of conflicting events where events +take place in distinct threads and at least one event is a write. -Applied to the above example, we encounter the following behavior. +## Example 4 -- Thread T0 processes *w*(*x*)1 and records that - *L**S*(*w*(*x*)) = {}. + T0 T1 Lockset + e1. fork(T1) + e2. acq(L1) + e3. acq(L2) + e4. wr(V2) {L1,L2} + e5. rel(L2) + e6. wr(V2) {L1} + e7. rel(L1) + e8. acq(L2) + e9. wr(V2) {L2} + e10. rel(L2) -- Once thread T0 processes *w*(*x*)3 and records that - *L**S*(*w*(*x*)) = {*y*}. +The write e4 in thread T0 is protected by locks L1 and L2. Hence, e4 is +not in a race with the write e9 (their locksets share the common lock +L2). On the other hand, write e6 is in a race with e9 (there is no +common lock). -- This means that the history of earlier locksets for writes on *x* is - lost. +## Example 5 -- This means that algorithms that only record locksets for most recent - writes/reads will not signal a data race here. + T0 T1 Lockset + e1. fork(T1) + e2. acq(L1) + e3. wr(V2) {} + e4. wr(V2) {L1} + e5. rel(L1) + e6. acq(L1) + e7. wr(V2) {L1} + e8. rel(L1) -## Example 3 +Write e3 takes place in thread T1 whereas the acquire and release take +place in thread T0. There is no synchronization between thread T0 and +thread T1. Hence, the lockset of write e3 is empty. Hence, the write e3 +is in a race with the write e4 (because their locksets are disjoint). - T0 T1 Lockset - 1. w(x) {} - 2. acq(y) - 3. rel(y) - 4. acq(y) - 5. w(x) {y} - 6. rel(y) +## Example 6 -Locksets are disjoint. Hence, the algorithm signals that there is a data -race. + T0 T1 T2 Lockset + e1. fork(T1) + e2. wr(V2) {} + e3. fork(T2) + e4. wr(V2) {} + e5. join(T0) + e6. wr(V2) {} -However, in the actual program, thread T0 forks thread T1. We assume -that after the release at trace position 3 there is a go statement to -create thread T1. For example, the above trace could result from the -following program. +The locksets of all writes are empty. Hence, we would issue the +following data race warnings. - x = 3 - acq(y) - rel(y) +- e2 is in a race with e4 - go func() { - acq(y) - x = 4 - rel(y) - }() +- e2 is in a race with e6 -This “fork” information is not recorded in the trace. As we only compare -locksets, we encounter here another case of a false positive. +- e4 is in a race with e6 -## Example 4 +The race warning “e2 is in a race with e4” is a false positive. Due to +the fork event e3, event e2 will always happen before event e4. - T0 T1 T2 Lockset - 1. acq(y) - 2. w(x) {} - 3. rel(y) - 4. acq(y) - 5. w(x) {y} - 6. rel(y) +The race warning “e2 is in a race with e6” is a false positive as well. +Due to the join event e5, event e2 will always happen before e6. + +The only true positive is “e4 is in a race with e6”. + +## Lockset implementation + +[Go playground](https://go.dev/play/p/AqXqUdS1muv) + +Check out main and the examples. + + package main + + // Lockset-based race predictor -Shouldn’t the lockset at trace position 2 include lock variable y!? + import "fmt" + import "strconv" + import "strings" -No! + // Example traces. -- The write at trace position 2 seems to be protected by lock variable - y. + // Traces are assumed to be well-formed. + // For example, if we fork(ti) we assume that thread ti exists. + + func trace_1() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + rel(t0, x), + acq(t1, x), + rel(t1, x), + wr(t1, z)} + } + + func trace_2() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + rel(t0, x), + wr(t1, z), + acq(t1, x), + rel(t1, x)} + + } + + func trace_2b() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t0, z), + wr(t0, z), + rel(t0, x), + wr(t1, z), + acq(t1, x), + rel(t1, x)} + + } + + func trace_3() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + x := 1 + z := 2 + return []Event{ + wr(t0, z), + fork(t0, t1), + fork(t0, t2), + rd(t0, z), + rd(t1, z), + acq(t2, x), + wr(t2, z), + rel(t2, x)} + + } + + func trace_3b() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + fork(t0, t2), + wr(t0, z), + rd(t0, z), + rd(t1, z), + acq(t2, x), + wr(t2, z), + rel(t2, x)} + + } -- However, thread T1 does not “own” this lock variable! + func trace_4() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + y := 2 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + acq(t0, y), + wr(t0, z), + rel(t0, y), + wr(t0, z), + rel(t0, x), + acq(t1, y), + wr(t1, z), + rel(t1, y)} + + } + + func trace_5() []Event { + t0 := mainThread() + t1 := nextThread(t0) + x := 1 + z := 2 + return []Event{ + fork(t0, t1), + acq(t0, x), + wr(t1, z), + wr(t0, z), + rel(t0, x), + acq(t1, x), + wr(t1, z), + rel(t1, x)} + } + + func trace_6() []Event { + t0 := mainThread() + t1 := nextThread(t0) + t2 := nextThread(t1) + z := 2 + return []Event{ + fork(t0, t1), + wr(t0, z), + fork(t0, t2), + wr(t2, z), + join(t1, t0), + wr(t1, z)} + } + + func main() { + + run(trace_1()) + + run(trace_2()) + + run(trace_2b()) + + run(trace_3()) + + run(trace_3b()) + + run(trace_4()) + + run(trace_5()) + + run(trace_6()) + + } + + /////////////////////////////////////////////////////////////// + // Helpers + + func max(x, y int) int { + if x < y { + return y + } + return x + } + + func debug(s string) { + fmt.Printf("%s", s) + + } + + /////////////////////////////////////////////////////////////// + // Events + + type EvtKind int + + const ( + AcquireEvt EvtKind = 0 + ReleaseEvt EvtKind = 1 + WriteEvt EvtKind = 2 + ReadEvt EvtKind = 3 + ForkEvt EvtKind = 4 + JoinEvt EvtKind = 5 + ) + + type Event struct { + k_ EvtKind + id_ int + a_ int + } + + func (e Event) thread() int { return e.id_ } + func (e Event) kind() EvtKind { return e.k_ } + func (e Event) arg() int { return e.a_ } + + // Some convenience functions. + func rd(i int, a int) Event { + return Event{ReadEvt, i, a} + } + + func wr(i int, a int) Event { + return Event{WriteEvt, i, a} + } + + func acq(i int, a int) Event { + return Event{AcquireEvt, i, a} + } + + func rel(i int, a int) Event { + return Event{ReleaseEvt, i, a} + } + + func fork(i int, a int) Event { + return Event{ForkEvt, i, a} + } + + func join(i int, a int) Event { + return Event{JoinEvt, i, a} + } + + // Trace assumptions. + // Initial thread starts with 0. Threads have ids in ascending order. + + func trace_info(es []Event) (int, map[int]bool, map[int]bool) { + max_tid := 0 + vars := map[int]bool{} + locks := map[int]bool{} + for _, e := range es { + max_tid = max(max_tid, e.thread()) + if e.kind() == WriteEvt || e.kind() == ReadEvt { + vars[e.arg()] = true + } + if e.kind() == AcquireEvt { // For each rel(x) there must exists some acq(x) + locks[e.arg()] = true + } + } + return max_tid, vars, locks + } + + func mainThread() int { return 0 } + func nextThread(i int) int { return i + 1 } + + const ( + ROW_OFFSET = 14 + ) + + // Omit thread + loc info. + func displayEvtSimple(e Event) string { + var s string + arg := strconv.Itoa(e.arg()) + switch { + case e.kind() == AcquireEvt: + s = "acq(L" + arg + ")" // L(ock) + case e.kind() == ReleaseEvt: + s = "rel(L" + arg + ")" + case e.kind() == WriteEvt: + s = "wr(V" + arg + ")" // V(ar) + case e.kind() == ReadEvt: + s = "rd(V" + arg + ")" + case e.kind() == ForkEvt: + s = "fork(T" + arg + ")" // T(hread) + case e.kind() == JoinEvt: + s = "join(T" + arg + ")" + } + return s + } + + func colOffset(i int, row_offset int) string { + n := (int)(i) + return strings.Repeat(" ", n*row_offset) + } + + // Thread ids fully cover [0..n] + func displayTraceWithLS(m int, es []Event, evt_ls map[int]LS, row_offset int) string { + s := "" + for i, e := range es { + ls_info := " " + _, ok := evt_ls[i] + if ok { + ls_info += evt_ls[i].display() + } + row := "\n" + "e" + strconv.Itoa(i+1) + ". " + colOffset(e.thread(), row_offset) + displayEvtSimple(e) + colOffset(m-e.thread(), row_offset) + ls_info + s = s + row + } + // Add column headings. + heading := " " + for i := 0; i <= m; i++ { + heading += "T" + strconv.Itoa(i) + strings.Repeat(" ", row_offset-2) + } + heading += "Lockset" + s = heading + s + + return s + } + + /////////////////////////////////////////////////////////////// + // Lock sets + + type LS map[int]bool // + + func (ls LS) add(x int) { + ls[x] = true + } + + func (ls LS) remove(x int) { + delete(ls, x) + } + + func (ls LS) display() string { + var s string + i := len(ls) + s = "{" + for lock, _ := range ls { + + if i > 1 { + s = s + "L" + strconv.Itoa(lock) + "," + + } + if i == 1 { + s = s + "L" + strconv.Itoa(lock) + } + i-- + } + return s + "}" + } + + func copyLS(ls LS) LS { + new := make(map[int]bool) + for lock, _ := range ls { + new[lock] = true + } + + return new + } + + /////////////////////////////////////////////////////////////// + + type State struct { + th_lockset map[int]LS // key = thread id + evt_lockset map[int]LS // key = trace position + } + + func run(es []Event) { + + var s State + + s.th_lockset = make(map[int]LS) + s.evt_lockset = make(map[int]LS) + + max_tid := 0 + + for _, e := range es { + max_tid = max(max_tid, e.thread()) + } + + for i := 0; i <= max_tid; i++ { + s.th_lockset[i] = make(map[int]bool) + } + + exec := func(e Event) { + switch { + case e.kind() == AcquireEvt: + s.acquire(e) + case e.kind() == ReleaseEvt: + s.release(e) + case e.kind() == ForkEvt: + s.fork(e) + case e.kind() == JoinEvt: + s.join(e) + case e.kind() == WriteEvt: + s.write(e) + case e.kind() == ReadEvt: + s.read(e) + } + + } + + for i, e := range es { + exec(e) + if e.kind() == WriteEvt { + s.evt_lockset[i] = copyLS(s.th_lockset[e.thread()]) + } + if e.kind() == ReadEvt { + s.evt_lockset[i] = copyLS(s.th_lockset[e.thread()]) + } + } + + fmt.Printf("\n%s\n", displayTraceWithLS(max_tid, es, s.evt_lockset, 12)) + + } + + func (s *State) acquire(e Event) { + t := e.thread() + y := e.arg() + + s.th_lockset[t].add(y) + + } + + func (s *State) release(e Event) { + t := e.thread() + y := e.arg() + s.th_lockset[t].remove(y) + } + + func (s *State) fork(e Event) { + + } + + func (s *State) join(e Event) { + + } + + func (s *State) write(e Event) { + + } + + func (s *State) read(e Event) { + + }