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.

Sign up for GitHub

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

Model Checked - MPSC queue + Rework State Machines #128

Merged
merged 14 commits into from
May 9, 2020
Merged

Model Checked - MPSC queue + Rework State Machines #128

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
1f70d6a
model checking - 1st try to fix MPSC queue (the model checker crashes…
mratsim May 9, 2020
fa881e8
Give the thread the opportunity to not deadlock on sleep on Mac/with …
mratsim May 9, 2020
bd762f9
whoopsie
mratsim May 9, 2020
ce8dfe0
Add impl of Weave MPSC channel in C++ for CDSChecker model checking +…
mratsim May 9, 2020
da5ae0b
Comment out GEMM tests for syncRoot + Pledges: https://github.com/mra…
mratsim May 9, 2020
4bb7916
don't use sleep, it's can deadlock in the CI ...
mratsim May 9, 2020
7b205b7
Try get epoch time to avoid mac bugs
mratsim May 9, 2020
5673eec
use `getTime` and hope that it's properly implemented on Mac
mratsim May 9, 2020
c31e45f
State-machine, return to CheckTask to avoid leaving task spawning mul…
mratsim May 9, 2020
82265ad
Don't spinlock for testing, deadlocks ARM and OSX
mratsim May 9, 2020
7c760dd
Could it be non-mono clock jitter?
mratsim May 9, 2020
cd116d0
Add some log for MacOS debug
mratsim May 9, 2020
efac680
Race condition between spawning the thread and entering the spinlock …
mratsim May 9, 2020
ea59771
a,d obviously I mess up the function call
mratsim May 9, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
21 changes: 21 additions & 0 deletions formal_verification/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
# Formal Verification

To ensure that Weave synchronization data structures are free of
concurrency bugs, deadlocks or livelocks they are formally verified via model checking.

The event notifier which parks idle threads and wake them up when receiving tasks
has been formally implemented verified via TLA+ (Temporal Logic of Action).

TLA+ is an industrial-strength formal specification language, model checker and can plug into proof assistant to prove properties of code.
It is used at Microsoft and Amazon to validate bug-free distributed protocol or at Intel to ensure that that the memory of a CPU is free of cache-coherency bugs.

Link: https://lamport.azurewebsites.net/tla/tla.html


Weave Multi-Producer Single-Consumer queue has been implemented in C++ and run through CDSChecker, a model checking tool for C++11 atomics.

It exhaustively checks all possible thread interleavings to ensure that no path lead to a bug.

Note: Due to CDSChecker running out of "snapshotting memory" (to rollback to a previous program state) when using dlmalloc `mspace` functions, the checks are not complete.

Link: http://plrg.ics.uci.edu/software_page/42-2/
Loading