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
# 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)) ())));
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev