Jonas Oberhauser
Jonas Oberhauser
If it's an internal limit, would it be much effort to switch to this: https://github.com/coq-community/aac-tactics ? This could also work for ∩ etc.
>I mean, IMM and RC11 would (likely) report the same races on the same C-code (cause they have the exact same definition of hb) Some RC11 graphs would never occur...
> In particular, no optimization eliminates data races. How sure are you about that? Do you have a full model of what the optimizations that you have enabled can do?
> > If I understood @camillegandotra correctly, you are also exploring relaxed versions of the locks which do not guarantee mutual exclusion (and can thus be racy). If this is...
> Can you share the output of `opam env` in your mingw shell? I can tell you how the output differs from what is there in a working environment: all...
> > I can tell you how the output differs from what is there in a working environment: all the paths (including paths unrelated to ocaml) are prefixed with `/cygdrive/c/...`...