Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Minimize redundancy in IOSimPOR logs #160

Open
1 task done
bolt12 opened this issue May 16, 2024 · 4 comments
Open
1 task done

Minimize redundancy in IOSimPOR logs #160

bolt12 opened this issue May 16, 2024 · 4 comments
Labels
enhancement New feature or request IOSimPOR Issues / PRs related to IOSimPOR trace Issues / PRs related to IOSim trace

Comments

@bolt12
Copy link
Contributor

bolt12 commented May 16, 2024

Is your feature request related to a problem? Please describe.

Recently I had to debug a IOSimPOR test failure (See #154) and although IOSimPOR is complicated, analysing the logs adds an extra layer of difficulty because the logs are quite large and have a lot of redundant information. I'll explain:

Here's the excerpt of a log for an IOSimPOR run with explorationDebugLevel = 2:

0s - Thread {1}.2 1 - Races {activeRaces = [StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}, stepInfoControl = ControlFollow [(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],5),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 4], effectWrites = fromList [TVarId 4], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],4),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],3),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [2], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [3]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],1),(ThreadId [],26)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [3], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],0),(ThreadId [],11)])}, stepInfoControl = ControlFollow [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)] [], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [4], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [4],1),(ThreadId [],26)])}, stepInfoControl = ControlAwait [ScheduleMod (RacyThreadId [4],2) ControlDefault [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)]], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 4], effectWrites = fromList [TVarId 4], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [3]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],0),(ThreadId [],11)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [4], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [4],0),(ThreadId [],15)])}, stepInfoControl = ControlAwait [ScheduleMod (RacyThreadId [4],2) ControlDefault [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)]], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [5], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 6], effectWrites = fromList [TVarId 6], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [5], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(RacyThreadId [5],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 4], effectWrites = fromList [TVarId 4], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [3]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],0),(ThreadId [],11)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [5], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [5],2),(ThreadId [],26)])}, stepInfoControl = ControlAwait [ScheduleMod (RacyThreadId [4],2) ControlDefault [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)]], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [2], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [3]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],0),(ThreadId [],11)])},Step {stepThreadId = RacyThreadId [4], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [4],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [4], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [4],0),(ThreadId [],15)])}], stepInfoRaces = []},StepInfo {stepInfoStep = Step {stepThreadId = RacyThreadId [5], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [5],1),(ThreadId [],26)])}, stepInfoControl = ControlAwait [ScheduleMod (RacyThreadId [4],2) ControlDefault [(RacyThreadId [3],0),(RacyThreadId [3],1),(RacyThreadId [3],2),(RacyThreadId [2],0),(RacyThreadId [3],3),(RacyThreadId [3],4),(RacyThreadId [3],5),(RacyThreadId [2],1),(RacyThreadId [2],2),(RacyThreadId [2],3),(RacyThreadId [2],4),(RacyThreadId [5],3),(RacyThreadId [5],4),(RacyThreadId [5],5),(RacyThreadId [1],0),(RacyThreadId [1],1),(RacyThreadId [1],2)]], stepInfoConcurrent = fromList [RacyThreadId [1],RacyThreadId [4],RacyThreadId [6],ThreadId []], stepInfoNonDep = [Step {stepThreadId = RacyThreadId [1], stepStep = 2, stepEffect = Effect {effectReads = fromList [TVarId 0], effectWrites = fromList [TVarId 0], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [1], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [1],0),(ThreadId [],3)])},Step {stepThreadId = RacyThreadId [2], stepStep = 4, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [5],RacyThreadId [6]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],4),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 3, stepEffect = Effect {effectReads = fromList [TVarId 3], effectWrites = fromList [TVarId 3], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],3),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],2),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 1, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],1),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 5, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],5),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 4, stepEffect = Effect {effectReads = fromList [TVarId 4], effectWrites = fromList [TVarId 4], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],4),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 3, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],3),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [2], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList [RacyThreadId [3]]}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 2, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [RacyThreadId [2]], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [2],0),(RacyThreadId [3],2),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],1),(ThreadId [],26)])},Step {stepThreadId = RacyThreadId [3], stepStep = 0, stepEffect = Effect {effectReads = fromList [], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [3],0),(ThreadId [],11)])},Step {stepThreadId = RacyThreadId [4], stepStep = 1, stepEffect = Effect {effectReads = fromList [TVarId 1], effectWrites = fromList [], effectForks = fromList [], effectThrows = [], effectWakeup = fromList []}, stepVClock = VectorClock (fromList [(RacyThreadId [4],1),(ThreadId [],26)])},...

This is only 1 line worth of trace out of 355 total lines, AND I had to truncate this line of code to not exceed GitHub's limit of 65k words. It has A LOT of useless information.

Describe the solution you'd like

Here's the data types involved in the trace I mentioned above:

type StepId = (IOSimThreadId, Int)

-- | A schedule modification inserted at given execution step.
--
data ScheduleMod = ScheduleMod{
    -- | Step at which the 'ScheduleMod' is activated.
    scheduleModTarget    :: StepId,
    -- | 'ScheduleControl' at the activation step.  It is needed by
    -- 'extendScheduleControl' when combining the discovered schedule with the
    -- initial one.
    scheduleModControl   :: ScheduleControl,
    -- | Series of steps which are executed at the target step.  This *includes*
    -- the target step, not necessarily as the last step.
    scheduleModInsertion :: [StepId]
  }
  deriving (Eq, Ord)


-- | Modified execution schedule.
--
data ScheduleControl = ControlDefault
                     -- ^ default scheduling mode
                     | ControlAwait [ScheduleMod]
                     -- ^ if the current control is 'ControlAwait', the normal
                     -- scheduling will proceed, until the thread found in the
                     -- first 'ScheduleMod' reaches the given step.  At this
                     -- point the thread is put to sleep, until after all the
                     -- steps are followed.
                     | ControlFollow [StepId] [ScheduleMod]
                     -- ^ follow the steps then continue with schedule
                     -- modifications.  This control is set by 'followControl'
                     -- when 'controlTargets' returns true.
  deriving (Eq, Ord, Show)

data Step = Step {
    stepThreadId :: !IOSimThreadId,
    stepStep     :: !Int,
    stepEffect   :: !Effect,
    stepVClock   :: !VectorClock
  }
  deriving Show

-- | As we execute a simulation, we collect information about each step.  This
-- information is updated as the simulation evolves by
-- `Control.Monad.IOSimPOR.Types.updateRaces`.
--
data StepInfo = StepInfo {
    -- | Step that we want to reschedule to run after a step in `stepInfoRaces`
    -- (there will be one schedule modification per step in
    -- `stepInfoRaces`).
    stepInfoStep       :: !Step,

    -- | Control information when we reached this step.
    stepInfoControl    :: !ScheduleControl,

    -- | Threads that are still concurrent with this step.
    stepInfoConcurrent :: !(Set IOSimThreadId),

    -- | Steps following this one that did not happen after it
    -- (in reverse order).
    stepInfoNonDep     :: ![Step],

    -- | Later steps that race with `stepInfoStep`.
    stepInfoRaces      :: ![Step]
  }
  deriving Show

--
-- Races
--

data Races = Races { -- These steps may still race with future steps
                     activeRaces   :: ![StepInfo],
                     -- These steps cannot be concurrent with future steps
                     completeRaces :: ![StepInfo]
                   }
  deriving Show

One can see how much information there's in each element of activeRaces or completeRaces fields. I propose either a refactorisation of these datatypes to avoid redundant information being stored, e.g.:

data StepInfo = StepInfo {
    -- | Step that we want to reschedule to run after a step in `stepInfoRaces`
    -- (there will be one schedule modification per step in
    -- `stepInfoRaces`).
    stepInfoStep       :: !Step,

    -- | Control information when we reached this step.
    stepInfoControl    :: !ScheduleControl,

    -- | Threads that are still concurrent with this step.
    stepInfoConcurrent :: !(Set IOSimThreadId),

    -- | Steps following this one that did not happen after it
    -- (in reverse order).
    stepInfoNonDep     :: ![IOSimThreadId],

    -- | Later steps that race with `stepInfoStep`.
    stepInfoRaces      :: ![IOSimThreadId]
  }
  deriving Show

and have a Map IOSimThreadId Step somewhere in the state. And the same for other similar places in the code.

OR

have a pretty printer with minimal verbosity that doesn't print all the information.

Are you willing to implement it?

  • Are you? 😃
@bolt12 bolt12 added the enhancement New feature or request label May 16, 2024
@coot
Copy link
Collaborator

coot commented Jul 3, 2024

I am not sure if I follow the suggested refactrosiation. Note that stepInfoNonDep and stepInfoRaces hold Steps different from the one in ``stepInfoStep. Each thread has many Step`s so `Map IOSimThreadId Step` won't help.

@bolt12
Copy link
Contributor Author

bolt12 commented Jul 3, 2024

The problem is that the show instance currently will print everything. The data types hold values of other data types that have quite a lot of data/text. My proposal is to refactor the data types to something more indirect at least for tracing. Instead of printing all text/data we print only the IDs (primary keys). These primary keys would still be able to fetch the required info because we would have Maps that held that info

@coot
Copy link
Collaborator

coot commented Jul 3, 2024

For that we'd need Map StepId Step, but that will be a large map holding all Steps, which has other downsides. I am not sure if optimising for pretty printing is the right way, so I'd prefer to have a nice pretty printer possibly with a verbosity parameter.

@bolt12
Copy link
Contributor Author

bolt12 commented Jul 3, 2024

That would work as well!

@coot coot added IOSimPOR Issues / PRs related to IOSimPOR trace Issues / PRs related to IOSim trace labels Oct 6, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request IOSimPOR Issues / PRs related to IOSimPOR trace Issues / PRs related to IOSim trace
Projects
None yet
Development

No branches or pull requests

2 participants