model-checker : remove unused argument in functions for heap comparison algorithm

[simgrid.git] / src / simix / smx_global.c

diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index eb2a141..130677a 100644 (file)
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -49,6 +49,7 @@ XBT_INLINE double SIMIX_timer_next(void)
 }
 
 /**
+ * \ingroup SIMIX_API
  * \brief Initialize SIMIX internal data.
  *
  * \param argc Argc
@@ -101,6 +102,7 @@ void SIMIX_global_init(int *argc, char **argv)
 }
 
 /**
+ * \ingroup SIMIX_API
  * \brief Clean the SIMIX simulation
  *
  * This functions remove the memory used by SIMIX
@@ -152,6 +154,7 @@ void SIMIX_clean(void)
 
 
 /**
+ * \ingroup SIMIX_API
  * \brief A clock (in second).
  *
  * \return Return the clock.
@@ -178,6 +181,10 @@ static int process_syscall_color(void *p)
   }
 }
 
+/**
+ * \ingroup SIMIX_API
+ * \brief Run the main simulation loop.
+ */
 void SIMIX_run(void)
 {
   double time = 0;
@@ -209,6 +216,11 @@ void SIMIX_run(void)
       /* WARNING, the order *must* be fixed or you'll jeopardize the simulation reproducibility (see RR-7653) */
 
       /* Here, the order is ok because:
+       *
+       *   Short proof: only maestro adds stuff to the process_to_run array, so the execution order of user contexts do not impact its order.
+       *
+       *   Long proof: processes remain sorted through an arbitrary (implicit, complex but fixed) order in all cases.
+       *
        *   - if there is no kill during the simulation, processes remain sorted according by their PID.
        *     rational: This can be proved inductively.
        *        Assume that process_to_run is sorted at a beginning of one round (it is at round 0: the deployment file is parsed linearly).