[isabelle-dev] Circular reasoning via multithreading seems too easy

[Peter Lammich]

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
>