From 8c1c47cfbf3410e87c6ef94d3336c33812d76398 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Thu, 4 Jun 2009 15:43:42 -0400 Subject: [PATCH] Update isched ooomem model Signed-off-by: Mathieu Desnoyers --- formal-model/ooomem-two-writes/mem.spin | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin index 9fc30cc..304c3f8 100644 --- a/formal-model/ooomem-two-writes/mem.spin +++ b/formal-model/ooomem-two-writes/mem.spin @@ -6,8 +6,8 @@ * * alpha = 0; * beta = 0; - * x = 2; - * y = 2; + * x = 1; + * y = 1; * * Process A Process B * alpha = 1; beta = 1; @@ -158,9 +158,8 @@ inline smp_mb() DECLARE_CACHED_VAR(byte, alpha, 0); DECLARE_CACHED_VAR(byte, beta, 0); -/* value 2 is uninitialized */ -byte read_one = 2; -byte read_two = 2; +byte read_one = 1; +byte read_two = 1; /* * Bit encoding, proc_one_produced : -- 2.34.1