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

[Makarius]

On 04/12/16 22:52, Peter Lammich wrote:
> 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. 

There might be something wrong at the very bottom (which I still need to
figure out later), but your kind of Isabelle/ML code would expose so
many other problems in practice that is unlikely to lead to a working tool.

This also explains why existing tools have never tripped this odd case,
because they use Isabelle/ML in a canonical (value-oriented) manner.


> 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.

It is about circularity. When implementing the parallel proof engine  in
2007/2008, I was aware that:

  (1) in practice, circularity hardly ever happens,

  (2) in theory, it might be a vector for attack.

So I added some complexity in the implementation to address that, but
that is still an unfinished area -- there are other conflicts with proof
terms in need of renovation.


Generically, Isabelle as a system is relatively hard to grasp. It is
surprising that it works so well, such that empirically most users think
that it is unbreakable.

This is mainly a social problem, and needs to be solved there.


	Makarius