On So, 2016-12-04 at 22:30 +0100, Makarius wrote: > On 04/12/16 11:14, Lars Hupel wrote: > > > > > > > > Where did you see these lots of Unsynchronized.ref (or better > > > Synchronized.var) in Isabelle Tools? > > There are 48 occurrences of "Unsynchronized.ref" in "~~/src/Tools", > > 181 > > in "~~/src/HOL", and some more in the AFP (many of which appear to > > be in > > generated code). > So what is wrong here?
I find it a bit scary that my first(!) naive attempt to trick Isabelle in presence of multithreading worked out immediately. I do not think that it is a desirable state that Isabelle's soundness depends on correct use of multithreading by the user/tools, and, at the same time, tools are using more and more multithreading. Btw: I do not believe that the error that I found depends on a (low- level) datarace, it should (not yet tried) also work out if using proper synchronization to make the tactic wait for the theorem. -- Peter > > Tending global state (normally via Synchronized.var and not the raw > Unsynchronized.ref) has been part of the normal routine of Isabelle > maintenance in the last 10 years. At the beginning almost nothing > worked, but around 2008/2009 it became routine. Today we have a > fairly > robust system, with lots of user tools that are mostly thread-safe. > > The "implementation" manual (sections 0.7.9 and 0.8) has some brief > explanations for users of Isabelle/ML. > > > Makarius > _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev