From: Mathieu Desnoyers Date: Thu, 4 Jun 2009 19:40:12 +0000 (-0400) Subject: Update ooo isched test X-Git-Tag: v0.1~196 X-Git-Url: http://git.liburcu.org/?p=urcu.git;a=commitdiff_plain;h=8e9a615359bed782ff5bf39e4b86d003c86a6701 Update ooo isched test Signed-off-by: Mathieu Desnoyers --- diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin index 1eb51c9..9fc30cc 100644 --- a/formal-model/ooomem-two-writes/mem.spin +++ b/formal-model/ooomem-two-writes/mem.spin @@ -6,13 +6,16 @@ * * alpha = 0; * beta = 0; + * x = 2; + * y = 2; * * Process A Process B * alpha = 1; beta = 1; * mb(); mb(); * x = beta; y = alpha; * - * if x = 1, then y = 1 when read. + * if x = 0, then y != 0 + * if y = 0, then x != 0 * * 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/read_order.ltl b/formal-model/ooomem-two-writes/read_order.ltl index f4dbf03..e0e986f 100644 --- a/formal-model/ooomem-two-writes/read_order.ltl +++ b/formal-model/ooomem-two-writes/read_order.ltl @@ -1 +1 @@ -[] (read_one_is_zero -> !read_two_is_zero) +[] (!(read_one_is_zero && read_two_is_zero))