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

[Peter Lammich]

Poking on the problem a bit more, I realized that, in the
Isabelle/jedit IDE, promises seem to be never checked. The following
theory works fine in the IDE, but, fortunately, fails in build mode.

I would have expected, at least at some point, to be notified of the
problem (mismatch of promised and proved thm) by the IDE. However, I
can even import Scratch.thy from some other theory, without ever seeing
any error in the IDE. 

--
  Peter


theory Scratch
imports Main
begin


ML ‹
  val thm_f = Future.fork (fn () => @{thm TrueI})
  val thm = Thm.future thm_f @{cprop False}
›

lemma F: False
  by (tactic ‹resolve_tac @{context} [thm] 1›)

(*ML ‹
  Thm.join_proofs [thm];
›*)

end



On So, 2016-12-04 at 23:13 +0100, Makarius wrote:
> 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
>