From 27afafe29f0395b9f70e7a7e71605598ae3015d3 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Fri, 15 May 2009 18:35:40 -0400 Subject: [PATCH] Update ooo mem model comments Signed-off-by: Mathieu Desnoyers --- formal-model/ooomem-double-update/mem.spin | 15 ++++++++++++++- formal-model/ooomem-two-writes/mem.spin | 15 ++++++++++++++- 2 files changed, 28 insertions(+), 2 deletions(-) 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 -- 2.34.1