[isabelle-dev] Fwd: [Isabelle-ci] Build failure in AFP

[Makarius]

On 31/08/18 22:00, Manuel Eberl wrote:
> 
> What puzzles me the most is the fact that this behaviour seems to depend
> on the underlying hardware, and it appears to be 100% reproducible on
> machines where it does happen. If this is a race condition, it must be
> one of the strangest one I have ever seen (note that it even happens in
> single-threaded mode).
> 
> Perhaps it might also be of interest to try this with different versions
> of Poly/ML, just to make sure it's not an issue with the underlying ML
> environment.

I see the same effect with Poly/ML 5.6 from Isabelle2017: a quite
different environment compared to Isabelle2018.

It requires the included change, and the following in
$ISABELLE_HOME_USER/etc/settings:

  init_component "$HOME/.isabelle/contrib/polyml-5.6-1"

Moreover, it probably requires this adhoc Unix environment variable:

  export LD_LIBRARY_PATH=$HOME/.isabelle/contrib/polyml-5.6-1/x86-linux


This is Ubuntu 16.04.5 LTS on Intel(R) Xeon(R) CPU E5-2620 v3 @ 2.40GHz.

What is actually your system where it happens to work?


	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1535749047 -7200
#      Fri Aug 31 22:57:27 2018 +0200
# Node ID a83229cc624d7236a2ef2158a33be611ae54500e
# Parent  dd44e31ca2c639b0915695c88020c14f044a73d8
test

diff -r dd44e31ca2c6 -r a83229cc624d src/Pure/Concurrent/single_assignment.ML
--- a/src/Pure/Concurrent/single_assignment.ML	Fri Aug 31 22:25:58 2018 +0200
+++ b/src/Pure/Concurrent/single_assignment.ML	Fri Aug 31 22:57:27 2018 +0200
@@ -55,7 +55,7 @@
           SOME _ => assign_fail name
         | NONE =>
             Thread_Attributes.uninterruptible (fn _ => fn () =>
-             (state := Set x; RunCall.clearMutableBit state; ConditionVar.broadcast cond)) ())));
+             (state := Set x; (* RunCall.clearMutableBit state; *) ConditionVar.broadcast cond)) ())));
 
 end;
 
diff -r dd44e31ca2c6 -r a83229cc624d src/Pure/Concurrent/synchronized.ML
--- a/src/Pure/Concurrent/synchronized.ML	Fri Aug 31 22:25:58 2018 +0200
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Aug 31 22:57:27 2018 +0200
@@ -54,7 +54,7 @@
           Immutable _ => immutable_fail name
         | Mutable _ =>
             Thread_Attributes.uninterruptible (fn _ => fn () =>
-             (state := Immutable x; RunCall.clearMutableBit state;
+             (state := Immutable x; (* RunCall.clearMutableBit state; *)
                ConditionVar.broadcast cond)) ())));