THIS REPOSITORY IS OUT-OF-DATE

ThreadSanitizer support has been integrated into OCaml and this repository is kept only for archiving purposes. For up-to-date information about using OCaml with ThreadSanitizer, you should read the dedicated OCaml manual page.

ThreadSanitizer support for OCaml 5

ThreadSanitizer is an effective approach to locate data races in concurrent code bases. This is an experimental extension of the OCaml compiler to add ThreadSanitizer support to OCaml 5.0.

Caveats

OCaml ThreadSanitizer support inherits the portability limitations of ThreadSanitizer: it is not available on Windows.
TSan investigates a particular execution and therefore will not detect races in code paths that are not visited.
TSan may still report false positives in some rare cases (see section 6.4 of the WBIA ’09 paper below).
Currently, ThreadSanitizer detection only works for native x86_64 executables; not bytecode programs, nor other architectures.

Trying it out

For Linux, you first need to install libunwind stack unwinding library on your system. Most Linux distributions provide a package.

Then you will need to work in a dedicated opam switch:

opam update
opam switch create 5.0.0+tsan

Building the switch may take a bit longer than usual due to some unavoidable ThreadSanitizer-incurred slowdowns in parts of the process. Expect a few minutes of build time.

On this switch, your programs will now be compiled with ThreadSanitizer instrumentation, including the packages you may install with opam.

If you link against C files, it is best to instrument them to detect data races in them as well, by passing -fsanitize=thread to GCC or clang. Note that if you use Dune, this setting can be added to a Dune profile by adding e.g. the following to your dune-workspace:

(env
 (tsan
  (c_flags -fsanitize=thread)))

Then you only need to select this profile, e.g. dune exec --profile tsan myexecutable.exe or dune runtest --profile tsan.

Examples

A simple race

The simplest of data races can be created by having two accesses to the same mutable location, one of them being a write:

type t = { mutable x : int }

let v = { x = 0 }

let () =
  let t1 = Domain.spawn (fun () -> v.x <- 10; Unix.sleep 1) in
  let t2 = Domain.spawn (fun () -> ignore v.x; Unix.sleep 1) in
  Domain.join t1;
  Domain.join t2

Running this program with ThreadSanitizer instrumentation will output a report looking like this:

==================
WARNING: ThreadSanitizer: data race (pid=4170290)
  Read of size 8 at 0x7f072bbfe498 by thread T4 (mutexes: write M0):
    #0 camlSimpleRace__fun_524 /tmp/simpleRace.ml:7 (simpleRace.exe+0x43dc9d)
    #1 camlStdlib__Domain__body_696 /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/stdlib/domain.ml:202 (simpleRace.exe+0x47b5dc)
    #2 caml_start_program ??:? (simpleRace.exe+0x4f51c3)
    #3 caml_callback_exn /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/callback.c:168 (simpleRace.exe+0x4c2b93)
    #4 caml_callback /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/callback.c:256 (simpleRace.exe+0x4c36e3)
    #5 domain_thread_func /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/domain.c:1093 (simpleRace.exe+0x4c6ad1)

  Previous write of size 8 at 0x7f072bbfe498 by thread T1 (mutexes: write M1):
    #0 camlSimpleRace__fun_520 /tmp/simpleRace.ml:6 (simpleRace.exe+0x43dc45)
    #1 camlStdlib__Domain__body_696 /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/stdlib/domain.ml:202 (simpleRace.exe+0x47b5dc)
    #2 caml_start_program ??:? (simpleRace.exe+0x4f51c3)
    #3 caml_callback_exn /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/callback.c:168 (simpleRace.exe+0x4c2b93)
    #4 caml_callback /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/callback.c:256 (simpleRace.exe+0x4c36e3)
    #5 domain_thread_func /home/olivier/.opam/5.0.0+tsan/.opam-switch/build/ocaml-variants.5.0.0+tsan/runtime/domain.c:1093 (simpleRace.exe+0x4c6ad1)

  Mutex M0 (0x000000567ad8) created at:
    #0 pthread_mutex_init /home/olivier/other_projects/llvm-project/compiler-rt/lib/tsan/rtl/tsan_interceptors_posix.cpp:1316 (libtsan.so.0+0x3cafb)
    [...]

SUMMARY: ThreadSanitizer: data race /tmp/simpleRace.ml:7 in camlSimpleRace__fun_524
==================
ThreadSanitizer: reported 1 warnings

If the mutable field is replaced with an Atomic reference, the warning disappears:

let v = Atomic.make 0

let () =
  let t1 = Domain.spawn (fun () -> Atomic.set v 10; Unix.sleep 1) in
  let t2 = Domain.spawn (fun () -> ignore (Atomic.get v); Unix.sleep 1) in
  Domain.join t1;
  Domain.join t2

Synchronization using an atomic variable

Synchronizing the two accesses above by busy-waiting on an atomic boolean will be detected by ThreadSanitizer and no data race will be reported:

type t = { mutable x : int }

let v = { x = 0 }

let v_modified = Atomic.make false

let () =
  let t1 =
    Domain.spawn (fun () ->
        v.x <- 10;
        Atomic.set v_modified true;
        Unix.sleep 1)
  in
  let t2 =
    Domain.spawn (fun () ->
        while not (Atomic.get v_modified) do () done;
        ignore v.x;
        Unix.sleep 1)
  in
  Domain.join t1;
  Domain.join t2

More efficiently, such synchronization can be implemented using a Mutex.t with the same result.

Background

There are two components to ThreadSanitizer (TSan): 1. A runtime library to track accesses to shared data and report races 2. A compiler instrumentation feature that inserts calls to that runtime library.

Internally the runtime library associates with each word of application memory at least 2 "shadow words". Each shadow word contains information about a recent memory access to that word, including a "scalar clock". Those clocks serve to establish a happens-before (HB) relation, i.e. an event orderings that we are certain of.

This information is maintained as a "shadow state" in a separate memory region, and updated at every (instrumented) memory access. A data race is reported every time two memory accesses are made to overlapping memory regions, and: - one of them is a write, and - there is no established happens-before relation between them. More information about TSan’s algorithm on their wiki.

Performance cost

ThreadSanitizer for OCaml incurs a slowdown and increases memory consumption. Preliminary benchmarks show a slowdown in the range 7x-13x and a memory consumption increase in the range 2x-7x.

Troubleshooting

OCaml-TSan is still considered experimental: although tested on large projects, there is a slight chance that it introduces crashes in your code. If you encounters problems using it, please do let us know and we will do our best to improve things.

Resources

Google Sanitizer wiki:
- TSan C/C++ Manual: https://github.com/google/sanitizers/wiki/ThreadSanitizerCppManual
- TSan Algorithm: https://github.com/google/sanitizers/wiki/ThreadSanitizerAlgorithm
A good talk about TSan’s internals: ""go test -race" Under the Hood" by Kavya Joshi
More information about the project status and technical details: https://github.com/ocaml-multicore/ocaml-tsan/wiki/Status-of-ThreadSanitizer-for-OCaml

License

ocaml-multicore/ocaml-tsan

ErrorLooks like something went wrong!

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors 297

Uh oh!

Languages

Error
Looks like something went wrong!

Packages