From: Martin Quinson <martin.quinson@loria.fr>
Date: Mon, 14 May 2012 13:46:53 +0000 (+0200)
Subject: add a short proof of corectness. should work too
X-Git-Tag: v3_7~5
X-Git-Url: http://info.iut-bm.univ-fcomte.fr/pub/gitweb/simgrid.git/commitdiff_plain/aae7a703c6ceea5834b33c55eea5076bf87a988b

add a short proof of corectness. should work too
---

diff --git a/src/simix/smx_global.c b/src/simix/smx_global.c
index eb2a14180f..3280f7a910 100644
--- a/src/simix/smx_global.c
+++ b/src/simix/smx_global.c
@@ -209,6 +209,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).