From: Mathieu Desnoyers Date: Fri, 15 May 2009 22:35:40 +0000 (-0400) Subject: Update ooo mem model comments X-Git-Tag: v0.1~221 X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=27afafe29f0395b9f70e7a7e71605598ae3015d3 Update ooo mem model comments Signed-off-by: Mathieu Desnoyers --- diff --git a/formal-model/ooomem-double-update/mem.spin b/formal-model/ooomem-double-update/mem.spin index 48c40f1..e033f67 100644 --- a/formal-model/ooomem-double-update/mem.spin +++ b/formal-model/ooomem-double-update/mem.spin @@ -1,5 +1,18 @@ /* - * mem.spin: Promela code to validate memory barriers with OOO memory. + * mem.spin: Promela code to validate memory barriers with out-of-order memory + * and out-of-order instruction scheduling. + * + * Algorithm verified : + * + * alpha = 0; + * beta = 0; + * + * Process A Process B + * alpha = 1; x = beta; + * wmb(); rmb(); + * beta = 1; y = alpha; + * + * if x = 1, then y will = 1 when it is read. * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin index 9202043..9c76c96 100644 --- a/formal-model/ooomem-two-writes/mem.spin +++ b/formal-model/ooomem-two-writes/mem.spin @@ -1,5 +1,18 @@ /* - * mem.spin: Promela code to validate memory barriers with OOO memory. + * mem.spin: Promela code to validate memory barriers with out-of-order memory + * and out-of-order instruction scheduling. + * + * Algorithm verified : + * + * alpha = 0; + * beta = 0; + * + * Process A Process B + * alpha = 1; beta = 1; + * wmb(); rmb(); + * x = beta; y = alpha; + * + * if x = 1, then y = 1 when read. * * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by