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

[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 <hupel at in.tum.de> 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5026 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20161205/3ca6f8fd/attachment.bin>