Documentation comments of TSan instrumentation choices #12694
Conversation
runtime/tsan.c
Outdated
| account. | ||
| - A field is accessed from C with `Field`, or more generally using a | ||
| `volatile value *` or a relaxed atomic access, and that field is modified | ||
| concurrently by OCaml code. Because caml_modify as a plain write for |
There was a problem hiding this comment.
This sentence is not so easy to understand for me. Maybe you could mention (with slightly more details) the translation / TSan effect of caml_modify and caml_initialize somewhere above, for example right before section 3.1?
There was a problem hiding this comment.
is a plain write?
This was a typo, thanks for spotting it. The right phrasing is: is instrumented as a plain write.
This sentence is not so easy to understand for me. Maybe you could mention (with slightly more details) the translation / TSan effect of caml_modify and caml_initialize somewhere above, for example right before section 3.1?
I added a paragraph about this. There was also a missing row in the table that I added.
runtime/tsan.c
Outdated
| the FFI rules on the condition that the GC does not run between the | ||
| allocation and the end of initialization) and a conflicting access is made | ||
| from OCaml after publication to other threads. There is no data race due | ||
| to data dependencies, but TSan does not take data dependencies into |
There was a problem hiding this comment.
The use of data dependency is still an open problem for FFI usage, so maybe one could write less affirmatively, “There should be no data race due to data dependency (see [MMMOC] in memory.c)”.
runtime/tsan.c
Outdated
| Our current make-do solution is that __tsan_volatile_readN performs a dummy | ||
| call to __tsan_atomic64_load, which is sufficient for correctness; and | ||
| __tsan_volatile_writeN simply calls __tsan_write8, i.e., volatile writes are | ||
| treated as plain writes. */ |
There was a problem hiding this comment.
I do not understand yet this part, could you clarify why having __tsan_atomic64_load vs. __tsan_write8 does what you want? (Is it related to the false positives mentioned in another PR? If so this might also be worth mentioning.)
|
Piggybacking on this PR to correct an outdated comment: diff --git a/runtime/tsan.c b/runtime/tsan.c
index 0a81f74ce1..8800eacdda 100644
--- a/runtime/tsan.c
+++ b/runtime/tsan.c
@@ -74,10 +74,10 @@
1.1 From OCaml
- Both `caml_raise_exn` and `caml_tsan_raise_notrace_exn` need to call
- `caml_tsan_exit_on_raise` to issue calls to `__tsan_func_exit` for each
- OCaml function exited by the exception. The process should be repeated
- when re-raising until the appropriate exception handler is found.
+ `caml_raise_exn` need to call `caml_tsan_exit_on_raise` to issue calls to
+ `__tsan_func_exit` for each OCaml function exited by the exception. The
+ process should be repeated when re-raising until the appropriate exception
+ handler is found.
1.2 From C
We have a removed |
|
Let me know if I should integrate this before merging or another PR should be opened. |
|
My plan is to wait an extra day before merging to let people make drive-by comments or last-minute changes. |
😅 Sorry, I noticed the mistake (or rather the outdated comment) when reviewing the PR, but I couldn't suggest the change at that moment. And I forgot to comment this right away, so it arrived lately! |
|
A |
|
Fixed. Should I squash the history? |
|
Yes please. |
Add a comment in tsan.c explaining the way OCaml accesses are signaled to TSan, and the consequences in terms of correct detection of data races. I also added a section explaining the choices made for volatile accesses. A case of TSan false positive in major_gc.c is commented with a pointer to these explanations. A not-completely-related outdated comment about exception raising and TSan was updated in the process.
OlivierNicole
force-pushed
the
tsan_mm_comments
branch
from
1df82c8
to
ab4278a
Compare
Add a comment in
tsan.cexplaining the way OCaml accesses are signaled to TSan, and the consequences in terms of correct detection of data races. I also added a section explaining the choices made forvolatileaccesses. A case of TSan false positive inmajor_gc.cis commented with a pointer to these explanations.