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

2016-12-16 Thread Makarius 
On 03/12/16 14:57, Peter Lammich wrote:
> 
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode 
> (isabelle build). 
> It just uses a prove_future, and proves the theorem with itself!

Here is the main result of investigating the sources and their entangled
history:

changeset:   64570:1134e4d5e5b7
user:wenzelm
date:Fri Dec 16 19:07:16 2016 +0100
files:   src/HOL/Library/Old_SMT/old_z3_proof_reconstruction.ML
src/HOL/SPARK/Tools/spark_vcs.ML src/Pure/Thy/thy_info.ML
src/Pure/more_thm.ML src/Pure/proofterm.ML src/Pure/thm.ML
description:
consolidate nested thms with persistent result, for improved performance;
always consolidate parts of fulfill_norm_proof: important to exhibit
cyclic thms (via non-termination as officially published), but this was
lost in f33d5a00c25d;


There was actually a second drop-out of formerly working behaviour (see
a2e7862e7dd5), but the changeset 1134e4d5e5b7 subsumes both, because the
consolidation of type thm/theory is now done a bit differently.

General concepts behind all that are described in section 3.2 in my
paper at ITP 2013, see especially the last two paragraphs.



Dropouts of this category belong to the normal routine in Isabelle,
according to its design principles in the last 10 years -- when we moved
from a research experiment towards a serious system. System reliability
has already reached a stage where most users never see it break down, so
any sense of what can go wrong is lost.

Hopefully this synthetic example helps to return to a better
understanding of what Isabelle really is: an increasing approximation of
ultimate perfection.

Whenever we reach that, the system will be discarded :-)


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-06 Thread Makarius 
On 05/12/16 17:13, Ondřej Kunčar wrote:
> 
> If you remove the call of the function Thm.name_derivation, the cycle gets 
> caught. The function
> is internally used in Goal.prove_future. It seems that the promises of the 
> theorem in question 
> are dropped in the function but we don’t understand whether this was intended 
> or not. 

This is what I have explained already abstractly: there is a conceptual
conflict of proof futures vs. proof terms (via
close_derivation/name_derivation).

Usually everything that is trivial or easy works properly in Isabelle.
Only hard problems are open, sometimes for years.

There might be a quick "fix", but such surgery usually degrades the
overall system quality. Isabelle development follows a different model.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-05 Thread Ondřej Kunčar 
Peter and I minimized the last example:

ML‹
 fun get_some var =
   case Synchronized.value var of
 NONE => (@{print} "defer"; get_some var)
   | SOME v => (@{print} "got it"; v)

 fun set var x =
   Synchronized.change var (K x)

 val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;

 val future_thm = Thm.future 
  (Future.fork (fn _ => get_some thm |> Thm.name_derivation "")) 
@{cprop "False"}

 val _ = set thm (SOME future_thm);

 val _ = Thm.join_proofs [future_thm]
›

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

If you remove the call of the function Thm.name_derivation, the cycle gets 
caught. The function
is internally used in Goal.prove_future. It seems that the promises of the 
theorem in question 
are dropped in the function but we don’t understand whether this was intended 
or not. 
Hopefully, this helps you to pin down the problem.

Bests,
Ondrej


> On 5 Dec 2016, at 11:12, Lars Hupel  wrote:
> 
>> 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.
> 
> For whatever it's worth, here's the same example with "Synchronized.var"
> and without a data race:
> 
> ML‹
>  fun get_some var =
>case Synchronized.value var of
>  NONE => (@{print} "defer"; get_some var)
>| SOME v => v
> 
>  fun set var x =
>Synchronized.change var (K x)
> 
>  val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;
> 
>  val _ =
>set thm (SOME
>  (Goal.prove_future @{context} [] [] @{prop "False"}
>(fn {context, ...} =>
>  ALLGOALS (resolve_tac context [get_some thm]
> ›
> 
> lemma F: False
>  by (tactic ‹resolve_tac @{context} [get_some thm] 1›)
> ___
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev



smime.p7s
Description: S/MIME cryptographic signature
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-05 Thread Makarius 
On 05/12/16 11:00, Peter Lammich wrote:
> 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. 

It is part of the current concepts of the Prover IDE that there is no
"closing" of the checking process. So the above behaviour is the
expected one.

Batch mode is different: it goes through great pains and complexity to
join all forks, and consolidate the type thm vs. theory content in the
end. (The problem encountered here is probably due to a conflict of this
documented / published approach vs. the actual implementation that has
to cope with proof terms and "close_derivation" as additional aspect.)


At some point, both the PIDE model and the batch checking should
converge to just one uniform approach: thus batch mode will become
slightly less strict, but interaction much more strict. It is just the
usual balancing of possibilities in a real system.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-05 Thread Lars Hupel 
> 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.

For whatever it's worth, here's the same example with "Synchronized.var"
and without a data race:

ML‹
  fun get_some var =
case Synchronized.value var of
  NONE => (@{print} "defer"; get_some var)
| SOME v => v

  fun set var x =
Synchronized.change var (K x)

  val thm: thm option Synchronized.var = Synchronized.var "hello" NONE;

  val _ =
set thm (SOME
  (Goal.prove_future @{context} [] [] @{prop "False"}
(fn {context, ...} =>
  ALLGOALS (resolve_tac context [get_some thm]
›

lemma F: False
  by (tactic ‹resolve_tac @{context} [get_some thm] 1›)
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-05 Thread 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
> 
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-04 Thread 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

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-04 Thread Lars Hupel 
>> 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?

Nothing, as far as I am concerned. I was merely trying to answer your
question.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-04 Thread Makarius 
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?

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

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

2016-12-04 Thread Peter Lammich 
This was an artificial counterexample, which I tried out of curiosity, but having applications like caching of already proved theorems in mind.Peter Originalnachricht Betreff: Re: [isabelle-dev] Circular reasoning via multithreading seems too easyVon: Makarius An: Peter Lammich ,isabelle-dev Cc: On 03/12/16 14:57, Peter Lammich wrote:> > the attached theory is accepted by all Isabelle's from 2015 to the> latest 2016-1-RC4, without any complaints, even in batch mode > (isabelle build). > It just uses a prove_future, and proves the theorem with itself!The behaviour is the same in Isabelle2014 and Isabelle2013, whichconforms to my intuition about this aspect of the system. It also meansit is not a regression, so not relevant for the Isabelle2016-1 release.I can't say on the spot what is going on, and if there is a genuineerror somewhere, but I can imagine a conflict of the existing dependencycheck of proof promises with PThm boxes of proof terms.In general, the thm type in Isabelle is definitely not what is beingtold in the common story about the "LCF approach", there is also not"the kernel" in Isabelle. We need to stop telling these tales.Did you encounter this situation in an actual application, or is it anartificially constructed counter-example? That makes an importantdifference, because it is theoretically obvious that Isabelle is not100% correct (just like Coq, HOL-Light, ...).	Makarius___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-04 Thread Lars Hupel 
> 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).
___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-03 Thread Makarius 
On 03/12/16 14:57, Peter Lammich wrote:
> 
> 2. Is there any simple coding policy that guarantees absence of such
> problems? Would be: "Do not store cterm/thm + everything containing it
> in references" enough, or perhaps: "Do not use Unsynchronized.ref at
> all"? (There are lots of usages of Unsynchronized.ref in the Isabelle 
> Tools).

Where did you see these lots of Unsynchronized.ref (or better
Synchronized.var) in Isabelle Tools?

In the last 10 years, we have got rid of most of this poking around in
mutable memory cells, and today it is mainly confined to system
infrastructure implementation, but not user tools.


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-03 Thread Makarius 
On 03/12/16 14:57, Peter Lammich wrote:
> 
> the attached theory is accepted by all Isabelle's from 2015 to the
> latest 2016-1-RC4, without any complaints, even in batch mode 
> (isabelle build). 
> It just uses a prove_future, and proves the theorem with itself!

The behaviour is the same in Isabelle2014 and Isabelle2013, which
conforms to my intuition about this aspect of the system. It also means
it is not a regression, so not relevant for the Isabelle2016-1 release.

I can't say on the spot what is going on, and if there is a genuine
error somewhere, but I can imagine a conflict of the existing dependency
check of proof promises with PThm boxes of proof terms.

In general, the thm type in Isabelle is definitely not what is being
told in the common story about the "LCF approach", there is also not
"the kernel" in Isabelle. We need to stop telling these tales.


Did you encounter this situation in an actual application, or is it an
artificially constructed counter-example? That makes an important
difference, because it is theoretically obvious that Isabelle is not
100% correct (just like Coq, HOL-Light, ...).


Makarius

___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

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

2016-12-03 Thread Peter Lammich 
Hi all,

the attached theory is accepted by all Isabelle's from 2015 to the
latest 2016-1-RC4, without any complaints, even in batch mode 
(isabelle build). 
It just uses a prove_future, and proves the theorem with itself!

So, I have two questions here:

1. I always thought that there is some tracking to avoid exactly those
situations, making the kernel robust against data races on the user-
level/in the tools. Is such a tracking possible, how hard would it be
to implement, and how much would it impact performance? I thought about
using level-1 proof terms to track theorem dependencies, and ensure
that they are non-circular, perhaps by simply numbering them in order
of occurrence. Would this be enough?

2. Is there any simple coding policy that guarantees absence of such
problems? Would be: "Do not store cterm/thm + everything containing it
in references" enough, or perhaps: "Do not use Unsynchronized.ref at
all"? (There are lots of usages of Unsynchronized.ref in the Isabelle 
Tools).

-- 
  Peter

-


theory Scratch
imports Main
begin

ML ‹
  val thm = Unsynchronized.ref @{thm TrueI};

  fun sleep 0 = ()
| sleep n = sleep (n-1)

  val _ = thm := (Goal.prove_future @{context} [] [] @{prop "False"}
(fn {context,...} 
=> ALLGOALS (sleep 1000; resolve_tac context [!thm])))
›

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

end



___
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev