After having read Matt Gallager's Mutexes and closure capture in Swift, I decided I would try to rewrite some of the classes in my Swift project which internally synchronize access to their members. Before trying to do so, however, I noticed something was missing from my current internal synchronization: tests that proved whether data races were actually prevented.
Intuitively, the locks "should work," and my program hasn't yet produced any data races (which signals that it at least mostly works) after hundreds of runs; but intuition doesn't always get so far with multi-threading, and not every edge case can be caught under normal conditions.
Sean Barry's article about writing unit tests to simulate race conditions, though helpful for testing the effects of race conditions, is not applicable since I'm concerned about testing data integrity (since race conditions are not the same as data races and don't need to always appear together) - not whether data is accessed in the correct order (of course, race conditions might lead to the wrong data being set at the end, but at least something legible would be there and/or it would make it there without crashing because of a simultaneous write)
How can I prove that my code prevents data races?
NOTE: The introduction of Swift actors will guarantee that my code is data race-free (though not race condition-free) and my classes will likely turn into actors; but since this question could be considered language-agnostic, it would still be good to know how to prove data races are prevented.
