some corrections (#68)

* some corrections

* fix singleton usage

* Update src/mmdata.h

Co-authored-by: Mario Carneiro <[email protected]>

* add attention tag again

* completely revert changes to the attention remark in nullPntrStruct.  This was accepted in a previous PR

* describe pools, fix the explanation of element at offset -3

* typo

* fix description of header element -3 again

* improve description of used block array

* typo

* fix brief description of free pool

* typo

Co-authored-by: Wolf Lammen <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>

Author: wlammen

src/metamath.c

@@ -61,9 +61,9 @@
 /*! \def MVERSION
  * The current version of metamath.  It is incremented each time the software
  * is modified.  When main versions are released, the version consists of a
- * main version, followed by a dot and a three-digit subversion.  Intermediate
- * versions are further followed by a free style suffix that should allow
- * ordering.
+ * major version, followed by a dot and a three-digit minor version.
+ * Pre-release versions are further followed by a free style suffix that
+ * should allow ordering.
  * The version string is extracted and then processed by shell and perl
  * scripts.  To avoid problems during replacements:
  * - use only printable characters from the ASCII range;

src/mmdata.c

@@ -97,12 +97,144 @@ vstring g_qsortKey; /* Used by qsortStringCmp; pointer only, do not deallocate *
 long poolAbsoluteMax = 1000000; /* Pools will be purged when this is reached */
 long poolTotalFree = 0; /* Total amount of free space allocated in pool */
 /*E*/long i1,j1_,k1; /* 'j1' is a built-in function */
+/*!
+ * \var void** memUsedPool
+ * \brief pointer to the pool of fragmented memory blocks
+ * Memory fragmentation is kept simple in Metamath.  If a block contains both
+ * consumed and free space, all of the free space is at the end.  Fragmented
+ * blocks with free space are kept in the used block array, that memUsedPool
+ * points to.  For the notion of block, suballocator see \a memFreePool.  This
+ * scheme supports in particular stack like memory, where data is pushed at and
+ * popped off the end.
+ *
+ * The used blocks array does initially not exist.  This is indicated by a
+ * null value.  Once this array is needed, space for it it is allocated from
+ * the system.
+ *
+ * The used block array may only be partially occupied, in which case elements
+ * at the end of the array are unused.  Its current usage is given by
+ * \a memUsedPoolSize.  Its current size including unused elements, is given by
+ * \a memUsedPoolMax.
+ *
+ * \invariant Each block in the used blocks array has its index noted in its
+ * hidden header, for backward reference.
+ * 
+ * \attention Desite the name of this variable fully occupied blocks are never
+ * kept in the used block array.
+ */
 void **memUsedPool = NULL;
+/*!
+ * \var long memUsedPoolSize
+ * \attention this is the number of individual blocks, not the accumulated
+ * (unused) bytes contained.
+ *
+ * The Metamath suballocator holds fragmented blocks in a used block array.
+ * The number of occupied entries is kept in this variable.  Elements at the
+ * end of the used block array may be unused.  The fill size is given by this
+ * variable.  For further information see \a memUsedPool.
+ *
+ * \invariant memUsedPoolSize <= \a memUsedPoolMax.
+ */
 long memUsedPoolSize = 0; /* Current # of partially filled arrays in use */
+/*!
+ * \var long memUsedPoolMax
+ * \attention this is the number of individual free blocks, not the accumulated
+ * bytes contained.
+ *
+ * The Metamath suballocator holds fragmented blocks in the used block
+ * array.  This array may only partially be occupied.  Its total capacity is
+ * kept in this variable.  For further information see \a memUsedPool.
+ *
+ * This variable may grow during a reallocation process.
+ *
+ * \invariant (memUsedPoolMax > 0) == (\a memUsedPool != 0) 
+ */
 long memUsedPoolMax = 0; /* Maximum # of entries in 'in use' table (grows
                                as nec.) */
+/*!
+ * \var void** memFreePool
+ * \brief pointer to the pool of completely free memory blocks
+ *
+ * **suballocator**
+ *
+ * Metamath does not free memory by returning it to the operating system again.
+ * Instead it has a suballocator that marks them as unused.  During execution
+ * chunks of memory become unused, either completely, or through fragmentation.
+ * The suballocator keeps track of these by entering them either into a free
+ * block array, or into a used block array.  The idea behind this suballocation
+ * scheme is to reduce the number of system malloc and alloc calls.
+ *
+ * Although the suballocator tries to avoid returning memory to the system, it
+ * can do so under extreme memory constraints.
+ *
+ * The suballocator is initially neither equipped with a free block array,
+ * pointed to by memFreePool, or a used block array, see \a memUsedPool.  Both
+ * are null then, but once memory is returned to the suballocator again, it
+ * allocates some space for the needed array.
+ *
+ * The free block array contains totally unused blocks.  The array may only
+ * partially be occupied, in which case The elements at the end are the unused
+ * ones.  Its current fill size is given by \a memFreePoolSize.  Its capacity
+ * is given by \a memFreePoolMax.
+ *
+ * Fragmented blocks are kept in a separate \a memUsedPool.  The suballocator
+ * never tracks fully used blocks.
+ *
+ * **block of memory**
+ *
+ * Each block used by the suballocater is formally treated as an array of
+ * pointer (void*).  It is divided into an administrative header, followed by
+ * elements reserved for application data.  The header is assigned elements -3
+ * to -1 in the formal array, so that application data starts with element 0.
+ * A pointer to the block always refers to element 0, so the header appears
+ * somewhat hidden.
+ *
+ * The header elements are reinterpreted as long integer.  The values support
+ * a stack, where data is pushed at and popped off the end during the course of
+ * execution.  The semantics of the header elements are:
+ *
+ * offset -1:\n
+ *   is the current size of the stack (in bytes, not elements!),
+ *   without header data. When interpreted as an offset into the stack, it
+ *   references the first element past the top of the stack.
+ *
+ * offset -2:\n
+ *   the allocated size of the array, in bytes, not counting the
+ *   header.  When used as a stack, it marks the limit where the stack
+ *   overflows.
+ *
+ * offset -3:\n
+ *   If this block has free space at the end (is fragmented), then it contains
+ *   its index in the used blocks array, see \a memUsedPool.  A value of -1
+ *   indicates it has no free space left, hence is not held in this pool.
+ */
 void **memFreePool = NULL;
+/*!
+ * \var long memFreePoolSize
+ * \attention this is the number of individual free blocks, not the accumulated
+ * bytes contained.
+ *
+ * The Metamath suballocator holds free blocks in a free block array.  The
+ * number of occupied entries is kept in this variable.  Elements at the end of
+ * the free block array may not be used.  The fill size is given by this
+ * variable.  For further information see \a memFreePool.
+ *
+ * \invariant memFreePoolSize <= \a memFreePoolMax.
+ */
 long memFreePoolSize = 0; /* Current # of available, allocated arrays */
+/*!
+ * \var long memFreePoolMax
+ * \attention this is the number of individual free blocks, not the accumulated
+ * bytes contained.
+ *
+ * The Metamath suballocator holds free blocks in a free block array.  It may
+ * only partially be occupied.  Its total capacity is kept in this variable.  For
+ * further information see \a memFreePool.
+ *
+ * This variable may grow during a reallocation process.
+ *
+ * \invariant (memFreePoolMax > 0) == (\a memFreePool != 0) 
+ */
 long memFreePoolMax = 0; /* Maximum # of entries in 'free' table (grows
                                as nec.) */
 

src/mmdata.h

@@ -21,7 +21,8 @@
  */
 typedef char flag;
 
-/*! 
+/*!
+ * \deprecated
  * \var flag g_listMode.
  * Obsolete.  Now fixed to 0.  Historically the metamath sources were also used
  * for other purposes than maintaining Metamath files.  One such application, a
@@ -51,19 +52,9 @@ typedef long nmbrString; /* String of numbers */
  * addressed with offsets -1 to -3 relative to the first element of the stack.
  * This allows for easy embedding of a stack within an even larger memory
  * pool.  The fields of this hidden structure, although formally pointers,
- * are loaded with long int values describing properties of the stack:
- *
- * offset -1: is the current size of the stack (in bytes, not elements!). When
- *   interpreted as an offset into the stack, it references the first element
- *   past the top of the stack.
- *
- * offset -2: the allocated size of the array, in bytes.  When used with a
- *   stack, it marks the limit where the stack overflows.  Current size
- *   <= allocated size is an invariant of this structure.
- *
- * offset -3.  If this array is a subarray (or sub-stack) of a larger pool of
- *  pointers, then it marks the offset in bytes of the heading structure in the
- *  larger pool.
+ * are loaded with long int values describing properties of the stack.
+ * 
+ * For details see \a memFreePool.
  */
 typedef void* pntrString; /* String of pointers */
 
@@ -276,19 +267,22 @@ struct nullPntrStruct {
      */
     long poolLoc;
     /*! 
-     * allocated size of the memory block containing the \a pntrString.
+     * allocated size of the memory block containing the \a pntrString,
+     * excluding any hidden administrative data.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
      * single void* instance. 
      */
     long allocSize;
     /*! 
-     * currently used size of the memory block containing the \a pntrString.
+     * currently used size of the memory block containing the \a pntrString,
+     * excluding any hidden administrative data.
      * Note: this is the number of bytes, not elements!  Fixed to the size of a
      * single pointer element.
      */
     long actualSize;
     /*! 
      * memory for a single void* instance, set and fixed to the null pointer.
+     * A null marks the end of the array.
      */
     pntrString nullElement; };
 /*!
@@ -299,6 +293,10 @@ struct nullPntrStruct {
  * \attention mark as const
  */
 extern struct nullPntrStruct g_PntrNull;
+/*!
+ * \def NULL_PNTRSTRING
+ * yields the address of a global null pointer element.
+ */
 #define NULL_PNTRSTRING &(g_PntrNull.nullElement)
 #define pntrString_def(x) pntrString *x = NULL_PNTRSTRING
 #define free_pntrString(x) pntrLet(&x, NULL_PNTRSTRING)