[isabelle-dev] Notes and updates on Isabelle/ML

[Makarius]

On Tue, 25 Mar 2014, Makarius wrote:

>   * pointer_eq is not part of SML and requires extra reasoning that it is
>     correct whenever it is used (normally in certain hot-spots of kernel
>     operations).  See also the surprise caused by some optimizations of
>     the Poly/ML runtime system concerning object identity, which are
>     perfectly inside the Standard ML semantics:
>     http://lists.inf.ed.ac.uk/pipermail/polyml/2014-January/001389.html
>
> Concerning the last point, I did not inspect the actual situation outside of 
> Isabelle/Pure yet.  It probably requires further looking, and more 
> explanations on either of the mailing lists.

This is still pending, and relevant for the release.

SML semantics works with structural mathematical equality of values. 
Pointer equality is provided in the common implementation as a concession 
to physical hacking, in order to *peek* at the accidental situation in the 
run-time system.  According to the SML semantics, the memory menagement is 
allowed to:

   (1) introduce pointer equality that was not there before, e.g. via
       sharing of structurally equal values;

   (2) eliminate pointer equality that was there before, e.g. due to
       optimizations in lock-free garbage collection on multiple cores.

Both happens in Poly/ML, (1) very often, (2) very rarely.


This means, the ancient programming technique to use pointer_eq to see if 
the ML user code has "touched" some value no longer works: the ML run-time 
system might have touched it instead.

This means, special care is required to use pointer_eq at all, and it is 
often better to avoid it before spending too much time thinking about its 
correctness.


Here are some observations on the use of pointer_eq in 
Isabelle/dc542b78ef0f (apart from the traditional special tricks in Pure):

   * src/HOL/Tools/Lifting/lifting_info.ML

     One occurence in theory data managed: some canonical idioms to
     merge/join tables.  It looks formally OK, but I did not check it
     semantically.

   * src/HOL/Tools/ATP/atp_problem_generate.ML

     Two occurrences that are not immediately clear.  Looks like plain
     structural equality could do the job.

   * src/HOL/Tools/BNF/bnf_def.ML

     fun maybe_restore lthy_old lthy =
       lthy |> not (pointer_eq (lthy_old, lthy)) ? Local_Theory.restore;

     This looks odd.  The normal idiom is to maintain an option value, to
     say when a value remains explicitly unchanged (NONE).  If this is too
     awkward here, one could try comparing the background theories via
     Theory.eq_thy instead (which is strictly speaking just another
     approximation, but a deterministic one).  One could also try to
     express the idea behind the uses of maybe_restore differently.

   * Metis has various optimizations using the "portable" alias
     pointerEqual. Hard to say if there are potential problems coming from
     it.  A quick experiment with an always false predicate (which is a
     correct approximation) makes metis very slow, but in most situations
     it still terminates.  (Shall we forward this to Joe Hurd?  For the
     Isabelle release, Metis is better left alone, though.)


 	Makarius