Document the way to safely destroy automatically managed pools.

Copied from Perforce
 Change: 182166
 ServerID: perforce.ravenbrook.com

mps/example/scheme/scheme-advanced.c

@@ -4581,6 +4581,7 @@ int main(int argc, char *argv[])
      check final consistency and warn you about bugs.  It also allows the
      MPS to flush buffers for debugging data, etc.  It's good practise
      to destroy MPS objects on exit if possible rather than just quitting. */
+  mps_arena_park(arena);
   mps_root_destroy(reg_root);
   mps_thread_dereg(thread);
   mps_ap_destroy(strong_buckets_ap);

mps/example/scheme/scheme.c

@@ -4460,6 +4460,7 @@ int main(int argc, char *argv[])
      check final consistency and warn you about bugs.  It also allows the
      MPS to flush buffers for debugging data, etc.  It's good practise
      to destroy MPS objects on exit if possible rather than just quitting. */
+  mps_arena_park(arena);
   mps_root_destroy(reg_root);
   mps_thread_dereg(thread);
   mps_ap_destroy(obj_ap);

mps/manual/source/guide/lang.rst

@@ -1227,6 +1227,7 @@ on.
 
 Here's the tear-down code from the toy Scheme interpreter::
 
+    mps_arena_park(arena);
     mps_ap_destroy(obj_ap);
     mps_pool_destroy(obj_pool);
     mps_chain_destroy(obj_chain);

mps/manual/source/topic/finalization.rst

@@ -178,6 +178,20 @@ Cautions
         deprecated. See Appendix A of :ref:`Boehm (2002) <BOEHM02>`
         for a discussion of this problem.
 
+    .. note::
+
+        You can safely destroy pools containing objects registered for
+        finalization if you follow the "safe tear-down" procedure
+        described under :c:func:`mps_pool_destroy`, but the objects do
+        not get finalized.
+
+        The only reliable way to ensure that all finalizable object
+        gets finalized is to maintain a table of :term:`weak
+        references (1)` to all such objects. The weak references don't
+        prevent the objects from being finalized, but you can iterate
+        over the list at an appropriate point and finalize any
+        remaining objects yourself.
+
 4.  Not all :term:`pool classes` support finalization. In general, only
     pools that manage objects whose liveness is determined by garbage
     collection do so. See the :ref:`pool`.

mps/manual/source/topic/pool.rst

@@ -81,6 +81,27 @@ making it available for allocation.
     :term:`allocation points` and :term:`segregated allocation caches`
     created in the pool.
 
+    .. warning::
+
+        It is not safe to destroy an :term:`automatically managed
+        <automatic memory management>` pool if it contains any objects
+        that are :term:`reachable` from your roots, or any objects
+        that have been registered for :term:`finalization` but not yet
+        finalized, and then to carry on running the :term:`garbage
+        collector`.
+
+        Our recommended approach is to destroy automatically managed
+        pools just before destroying the arena, and then only while
+        the arena is in the :term:`parked state`. Thus a safe
+        tear-down sequence looks like this::
+
+            mps_arena_park(arena);
+            /* destroy threads and roots belonging to the arena */
+            /* destroy allocation points and caches belonging to the pool */
+            mps_pool_destroy(pool);
+            /* destroy chains and formats belonging to the arena */
+            mps_arena_destroy(arena);
+
 
 .. index::
    single: pool class