diff mbox

[cxx-mem-model] testing infrastructure

Message ID 4D792D6E.4050803@redhat.com
State New
Headers show

Commit Message

Aldy Hernandez March 10, 2011, 7:58 p.m. UTC
Hi folks.

The following is a test harness for testing atomicity problems and data 
races in multi-threaded environments.  Please see the README file in the 
patch below, which describes the use of GDB to test in-between states in 
a possibly threaded execution.

I would like to use this branch as the repository for tests of data 
races introduced by the compiler (atomics, illegal memory hoists of 
global variables in a multi-threaded environment, etc etc).

Eventually, as part of this project, I will be adding flags to the 
compiler (-fno-allow-load-data-races, etc), which we can use to safe 
guard against these illegal data race injections by the compiler.  Until 
then, I expect all (or most) of the tests below to fail.

A few tidbits...

1. I stole the GDB checks in the guality harness to check the presence 
of GDB.  If there is a more canonical way of checking the presence of a 
working gdb, let me know.

2. There is a README explaining the infrastructure, and the anatomy of a 
test.

3. Most of this work is actually Andrew Macleod's, who is off in a 
tropical island somewhere.  I have stolen most of his tests, implemented 
the harness, and cleaned up things for submission.  All errors, are 
obviously mine.

I would appreciate comments, and/or new relevant tests/problems you have 
encountered and would like fixed in the future.  I know there are a few 
Linux kernel problems that fall into this category.

Fire away, I don't mind being crucified.
Aldy
* lib/gcc-memmodel-gdb-test.exp: New.
	* gcc.dg/memmodel/speculative-store.c: New
	* gcc.dg/memmodel/subfields: New
	* gcc.dg/memmodel/guality.h: New
	* gcc.dg/memmodel/memmodel.h: New
	* gcc.dg/memmodel/global-hoist.c: New
	* gcc.dg/memmodel/d2.c: New
	* gcc.dg/memmodel/d3.c: New
	* gcc.dg/memmodel/memmodel.gdb: New.
	* gcc.dg/memmodel/memmodel.exp: New.
	* gcc.dg/memmodel/README: New.
	* g++.dg/memmodel/guality.h: New.
	* g++.dg/memmodel/memmodel.h: New.
	* g++.dg/memmodel/memmodel.gdb: New.
	* g++.dg/memmodel/memmodel.exp: New.
	* g++.dg/memmodel/atomics-1.C: New.

Comments

Aldy Hernandez March 10, 2011, 8:01 p.m. UTC | #1
Oh BTW, I have committed the aforementioned patch.  This is one of the 
benefits of having your own branch (and Andrew being on vacation).  You 
commit at will, and only later hide your head in shame after multiple 
flames-- correcting patches after the fact.
Mike Stump March 10, 2011, 9:09 p.m. UTC | #2
On Mar 10, 2011, at 11:58 AM, Aldy Hernandez wrote:
> The following is a test harness for testing atomicity problems and data races in multi-threaded environments.

The idea of developing a methodology for testing corner cases I think is interesting and neat.  volatile would be another area that one could use this sort of testing for, if they want.  As time goes on, I suspect we'll have an ever increasing need to handle multicore issues, so, I think expanding in this area is worthwhile.

There is a speed hit and the requirement to have a target (or simulator) for testing.  If one just checks generated assembly, one avoids needing a target, and avoids the speed hit, but at the cost of having to come up with assembles to match for the target, which is annoying.  I can imagine validating sequences with this sort of test suite and then for future testing, checking the cache for a sequence that is known to be ok, to speed testing.  I'll just note that this sort of speed hack is orthogonal and could be used for a large number of execute test cases, not just this class of testing.
diff mbox

Patch

Index: lib/gcc-memmodel-gdb-test.exp
===================================================================
--- lib/gcc-memmodel-gdb-test.exp	(revision 0)
+++ lib/gcc-memmodel-gdb-test.exp	(revision 0)
@@ -0,0 +1,67 @@ 
+#   Copyright (C) 2011 Free Software Foundation, Inc.
+
+# 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
+# the Free Software Foundation; either version 3 of the License, or
+# (at your option) any later version.
+#
+# This program is distributed in the hope that it will be useful,
+# but WITHOUT ANY WARRANTY; without even the implied warranty of
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+# GNU General Public License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with GCC; see the file COPYING3.  If not see
+# <http://www.gnu.org/licenses/>.
+
+# Utility for running a given test through the memmodel harness using gdb.
+# This is invoked via dg-final.
+#
+# Adapted from the guality harness.
+#
+# Call 'fail' if a given test printed "FAIL:", otherwise call 'pass'.
+
+proc memmodel-gdb-test { } {
+    if { ![isnative] || [is_remote target] } { return }
+
+    # This assumes that we are three frames down from dg-test, and that
+    # it still stores the filename of the testcase in a local variable "name".
+    # A cleaner solution would require a new DejaGnu release.
+    upvar 2 name testcase
+    upvar 2 prog prog
+    upvar 2 srcdir testsuite_dir
+
+    set gdb_name $::env(GUALITY_GDB_NAME)
+    set exec_file "[file rootname [file tail $prog]].exe"
+    set cmd_file "$testsuite_dir/gcc.dg/memmodel/memmodel.gdb"
+
+    send_log "Spawning: $gdb_name -nx -nw -quiet -x $cmd_file ./$exec_file\n"
+    set res [remote_spawn target "$gdb_name -nx -nw  -x $cmd_file ./$exec_file"]
+    if { $res < 0 || $res == "" } {
+	unsupported "$testcase"
+	return
+    }
+
+    remote_expect target [timeout_value] {
+	-re "FAIL:" {
+	    fail "$testcase"
+	    remote_close target
+	    return
+	}
+	# Too old GDB
+	-re "Unhandled dwarf expression|Error in sourced command file" {
+	    unsupported "$testcase"
+	    remote_close target
+	    return
+	}
+	timeout {
+	    unsupported "$testcase"
+	    remote_close target
+	    return
+	}
+    }
+
+    remote_close target
+    pass "$testcase"
+    return
+}
Index: gcc.dg/memmodel/speculative-store.c
===================================================================
--- gcc.dg/memmodel/speculative-store.c	(revision 0)
+++ gcc.dg/memmodel/speculative-store.c	(revision 0)
@@ -0,0 +1,51 @@ 
+/* { dg-do link } */
+/* { dg-options "-O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+/* FIXME: I can't get this to fail.  */
+
+#include <stdio.h>
+#include "memmodel.h"
+
+/* This file tests that speculative store movement out of a loop doesn't 
+   happen.  This is disallowed when -fno-allow-store-data-races is on.  */
+
+int global = 100;
+
+/* Other thread makes sure global is 100 before the next instruction is
+ * exceuted.  */
+int memmodel_other_threads() 
+{
+  global = 100;
+}
+
+int memmodel_step_verify()
+{
+  if (global != 100)
+    {
+      printf("FAIL: global variable was assigned to.  \n");
+      return 1;
+    }
+}
+
+int memmodel_final_verify()
+{
+  return 0;
+}
+
+/* The variable global should never be assigned if func(0) is called.
+   This tests store movement out of loop thats never executed. */
+void test (int y)
+{
+  int x;
+  for (x=0; x< y; x++)
+    {
+       global = y;   /* This should never speculatively execute.  */
+    }
+}
+
+int main()
+{
+  test(0);
+  memmodel_done();
+}
Index: gcc.dg/memmodel/subfields.c
===================================================================
--- gcc.dg/memmodel/subfields.c	(revision 0)
+++ gcc.dg/memmodel/subfields.c	(revision 0)
@@ -0,0 +1,88 @@ 
+/* { dg-do link } */
+/* { dg-options "-O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+/* FIXME: I can't get this to fail.  */
+
+#include <stdio.h>
+#include "memmodel.h"
+
+/* This test verifies that data races aren't introduced by structure subfield 
+   stores. */
+
+struct test_struct {
+  char a;
+  char b;
+  char c;
+  char d;
+} var = {0,0,0,0};
+
+
+/* This routine sets field a to 'x'.  If executed properly, it will
+   not affect any of the other fields in the structure.  An improper
+   implementation may load an entire word, change the 8 bits for field
+   'a' and write the entire word back out. */
+void set_a(char x)
+{
+  var.a = x;
+}
+
+static int global = 0;
+
+/* The other thread increments the value of each of the other fields
+   in the structure every cycle.  If the store to the 'a' field does
+   an incorrect full or partial word load, mask and store, it will
+   write back an incorrect value to one or more of the other
+   fields.  */
+void memmodel_other_threads() 
+{
+  global++;
+  var.b = global;
+  var.c = global;
+  var.d = global;
+}
+
+
+/* Make sure that none of the other fields have been changed.  */
+int memmodel_step_verify()
+{
+  int ret = 0;
+  if (var.b != global)
+    {
+      printf("FAIL: Unexpected value. var.b is %d, should be %d\n",
+	     var.b, global);
+      ret = 1;
+    }
+  if (var.c != global)
+    {
+      printf("FAIL: Unexpected value. var.c is %d, should be %d\n",
+	     var.c, global);
+      ret = 1;
+    }
+  if (var.d != global)
+    {
+      printf("FAIL: Unexpected value. var.d is %d, should be %d\n",
+	     var.d, global);
+      ret = 1;
+    }
+  return ret;
+}
+
+/* Verify that every variable has the correct value.  */
+int memmodel_final_verify()
+{
+  int ret = memmodel_step_verify();
+  if (var.a != 1)
+    {
+      printf("FAIL: Unexpected value. var.a is %d, should be %d\n", var.a, 1);
+      ret = 1;
+    }
+  return ret;
+}
+
+int main ()
+{
+  set_a(1);
+  memmodel_done();
+  return 0;
+}
Index: gcc.dg/memmodel/guality.h
===================================================================
--- gcc.dg/memmodel/guality.h	(revision 0)
+++ gcc.dg/memmodel/guality.h	(revision 0)
@@ -0,0 +1 @@ 
+#include "../../gcc.dg/guality/guality.h"
Index: gcc.dg/memmodel/memmodel.h
===================================================================
--- gcc.dg/memmodel/memmodel.h	(revision 0)
+++ gcc.dg/memmodel/memmodel.h	(revision 0)
@@ -0,0 +1,7 @@ 
+int memmodel_fini = 0;
+
+void
+memmodel_done ()
+{
+  memmodel_fini = 1;
+}
Index: gcc.dg/memmodel/global-hoist.c
===================================================================
--- gcc.dg/memmodel/global-hoist.c	(revision 0)
+++ gcc.dg/memmodel/global-hoist.c	(revision 0)
@@ -0,0 +1,73 @@ 
+/* { dg-do link } */
+/* { dg-options "-O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+/* Verify that a load of a global is not hoisted out of a loop.  This
+   can introduce a data race, and is dissallowed if
+   -fno-allow-load-data-races is enabled. */
+
+#include <stdio.h>
+#include <stdlib.h>
+#include "memmodel.h"
+
+int global = 0;
+int sum[5];
+
+
+/* The other thread in the system increments the value of global by
+   one each time it is executed.  By accessing 'global' in a loop, we can
+   check if the load has been hoisted out of the loop by seeing if
+   iterations of the loop get the same or different values of
+   global.  */
+void
+memmodel_other_threads() 
+{
+  global++;
+}
+
+/* Nothing to verify at each step. */
+int
+memmodel_step_verify()
+{
+  return 0;
+}
+
+/* Every element of the array should have a different value of global if the 
+ * load is left in the loop like it is supposed to.  */
+int
+memmodel_final_verify()
+{
+  int ret = 0;
+  int x, y;
+
+  for (x = 0; x < 4; x++)
+    for (y = x + 1; y < 5; y++)
+      {
+	if (sum[x] == sum[y])
+	  {
+	    printf("FAIL: sum[%d] and sum[%d] have the same value : %d\n",
+		   x, y, sum[x]);
+	    ret = 1;
+	  }
+      }
+  return ret;
+}
+
+/* 'global' is bumped by "the other thread" every insn.  Test that all
+   elements of 'sum' are different, otherwise load of 'global' has
+   been hoisted.  */
+void
+test()
+{
+  int x;
+
+  for (x=0; x< 5; x++)
+    sum[x] =  global;
+}
+
+int
+main()
+{
+  test();
+  memmodel_done();
+}
Index: gcc.dg/memmodel/d2.c
===================================================================
--- gcc.dg/memmodel/d2.c	(revision 0)
+++ gcc.dg/memmodel/d2.c	(revision 0)
@@ -0,0 +1,60 @@ 
+/* { dg-do link } */
+/* { dg-options "-O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+#include <stdio.h>
+#include "memmodel.h"
+
+/* This is a variation on global-hoist.c where instead of a loop, we
+   store global into different elements of an array in straightline
+   code with an if condition.  This will catch cases where commoning
+   should be disabled when -fno-allow-load-data-races is on.  */
+
+/* Test the FALSE path in test.  */
+
+int global = 0;
+int sum[4] = { 0, 0, 0, 0 };
+
+void memmodel_other_threads() 
+{
+  global++;
+}
+
+int memmodel_step_verify()
+{
+  return 0;
+}
+
+int memmodel_final_verify()
+{
+  int ret = 0;
+  int x, y;
+  for (x = 0; x < 3; x++)
+    for (y = x + 1; y < 4; y++)
+      {
+	if (sum[x] == sum[y])
+	  {
+	    printf("FAIL: sum[%d] and sum[%d] have the same value : %d\n",
+		   x, y, sum[x]);
+	    ret = 1;
+	  }
+      }
+}
+
+/* Since global is always being increased by the 'other' thread, all
+   elements of sum should be different.  (no cse) */
+int test (int y)
+{
+  sum[0] = global;
+  if (y)
+    sum[1] = global;
+  else
+    sum[2] = global;
+  sum[3] = global;
+}
+
+int main()
+{
+  test(0);
+  memmodel_done();
+}
Index: gcc.dg/memmodel/d3.c
===================================================================
--- gcc.dg/memmodel/d3.c	(revision 0)
+++ gcc.dg/memmodel/d3.c	(revision 0)
@@ -0,0 +1,61 @@ 
+/* { dg-do link } */
+/* { dg-options "-O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+#include <stdio.h>
+#include "memmodel.h"
+
+/* A variation on global-hoist.c where instead of a loop, we store
+   global into different elements of an array in straightline code
+   with an if condition.  This will catch cases where commoning should
+   be disabled when -fno-allow-load-data-races is on.  */
+
+/* Test the TRUE path in test.  */
+
+int global = 0;
+int sum[4] = { 0, 0, 0, 0 };
+
+void memmodel_other_threads() 
+{
+  global++;
+}
+
+int memmodel_step_verify()
+{
+  return 0;
+}
+
+int memmodel_final_verify()
+{
+  int ret = 0;
+  int x, y;
+  for (x = 0; x < 3; x++)
+    for (y = x + 1; y < 4; y++)
+    {
+       if (sum[x] == sum[y])
+         {
+	   printf("FAIL: sum[%d] and sum[%d] have the same value : %d\n",
+		  x, y, sum[x]);
+	   ret = 1;
+	 }
+    }
+}
+
+/* Since global is always being increased by the 'other' thread, all
+   elements of sum should be different.  (No CSE) */
+int test(int y)
+{
+  sum[0] = global;
+  if (y)
+    sum[1] = global;
+  else
+    sum[2] = global;
+  sum[3] = global;
+}
+
+
+int main()
+{
+  test(1);
+  memmodel_done();
+}
Index: gcc.dg/memmodel/memmodel.gdb
===================================================================
--- gcc.dg/memmodel/memmodel.gdb	(revision 0)
+++ gcc.dg/memmodel/memmodel.gdb	(revision 0)
@@ -0,0 +1,13 @@ 
+break main
+run
+
+set $ret = 0
+while memmodel_fini != 1
+  call memmodel_other_threads()
+  stepi
+  set $ret |= memmodel_step_verify()
+end
+
+set $ret |= memmodel_final_verify()
+continue
+quit $ret
Index: gcc.dg/memmodel/memmodel.exp
===================================================================
--- gcc.dg/memmodel/memmodel.exp	(revision 0)
+++ gcc.dg/memmodel/memmodel.exp	(revision 0)
@@ -0,0 +1,49 @@ 
+# Your run of the mill dg test, but verify that we have a working GDB first.
+
+load_lib gcc-dg.exp
+load_lib gcc-memmodel-gdb-test.exp
+
+proc check_guality {args} {
+    set result [eval check_compile guality_check executable $args "-g -O0"]
+    set lines [lindex $result 0]
+    set output [lindex $result 1]
+    set ret 0
+    if {[string match "" $lines]} {
+      set execout [gcc_load "./$output"]
+      set ret [string match "*1 PASS, 0 FAIL, 0 UNRESOLVED*" $execout]
+    }
+    remote_file build delete $output
+    return $ret
+}
+
+dg-init
+
+# Test the presence of gdb with the guality infrastructure.
+global GDB
+if ![info exists ::env(GUALITY_GDB_NAME)] {
+    if [info exists GDB] {
+	set guality_gdb_name "$GDB"
+    } else {
+	set guality_gdb_name "[transform gdb]"
+    }
+    setenv GUALITY_GDB_NAME "$guality_gdb_name"
+}
+if {[check_guality "
+  #include \"$srcdir/$subdir/guality.h\"
+  volatile long int varl = 6;
+  int main (int argc, char *argv\[\])
+  {
+    GUALCHKVAL (varl);
+    return 0;
+  }
+"]} {
+  dg-runtest [lsort [glob $srcdir/$subdir/*.c]] "-g" ""
+# Uncomment line below when we have common C/C++ tests.
+#  dg-runtest [lsort [glob $srcdir/c-c++-common/memmodel/*.c]] "-g" ""
+}
+
+if [info exists guality_gdb_name] {
+    unsetenv GUALITY_GDB_NAME
+}
+
+dg-finish
Index: gcc.dg/memmodel/README
===================================================================
--- gcc.dg/memmodel/README	(revision 0)
+++ gcc.dg/memmodel/README	(revision 0)
@@ -0,0 +1,102 @@ 
+OVERVIEW
+--------
+
+This is a harness to test the atomicity of certain operations, and to
+make sure the compiler does not introduce data races in a
+multi-threaded environment.
+
+The basic premise is that we set up testcases such that the thing we
+want test, say an atomic instruction which stores a double word is in
+a function of its own.  We then run this testcase within GDB,
+controlled by a gdb script (memmodel.gdb).  The gdb script will break
+on the function to be tested, and then single step through every
+machine instruction in the function.  We set this up so GDB can make a
+couple of inferior function calls before and after each of these
+single step instructions for a couple of purposes:
+
+       1.  One of the calls simulates another thread running in the
+           process which changes or access memory.
+
+       2.  The other calls are used to verify that we always get the
+           expected behavior.
+
+For example, in the case of an atomic store, anyone looking at the
+memory associated with an atomic variable should never see any in
+between states. If you have an atomic long long int, and it starts
+with the value 0, and you write the value MAX_LONG_LONG, any other
+thread looking at that variable should never see anything other than 0
+or MAX_LONG_LONG.  If you implement the atomic write as a sequence of
+2 stores, it is possible for another thread to read the location after
+the first store, but before the second one is complete. That thread
+would then see an in-between state (one word would still be 0).
+
+We simulate this in the testcase by having GDB step through the
+program, instruction by instruction, and after each step, making an
+inferior function call which looks at the value of the atomic variable
+and verifies that it sees either 0 or MAX_LONG_LONG.  If it sees any
+other value, it fails the testcase.
+
+This way, we are *sure* there is no in between state because we
+effectively acted like an OS and switched to another thread after
+every single instruction of the routine is executed and looked at the
+results each time.
+
+We use the same idea to test for data races to see if an illegal load
+has been hoisted, or that two parallel bitfield writes don't overlap
+in a data race.
+
+Below is a skeleton of how a test should look like.  For more details,
+look at the tests themselves.
+
+ANATOMY OF A TEST
+-----------------
+
+/* { dg-do link } */
+/* { dg-options "-some-flags" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+/* NOTE: Any failure must be indicated by displaying "FAIL:".  */
+
+#include "memmodel.h"
+
+/* Called before each instruction, simulating another thread
+   executing.  */
+void memmodel_other_threads()
+{
+}
+
+/* Called after each instruction.  Returns 1 if any inconsistency is
+   found, 0 otherwise.  */
+int memmodel_step_verify()
+{
+  if (some_problem)
+    {
+      printf("FAIL: reason\n");
+      return 1;
+    }
+  return 0;
+}
+
+/* Called at the end of the program (memmodel_fini == 1).  Verifies
+   the state of the program and returns 1 if any inconsistency is
+   found, 0 otherwise.  */
+int memmodel_final_verify()
+{
+  if (some_problem)
+    {
+      printf("FAIL: reason\n");
+      return 1;
+    }
+  return 0;
+}
+
+int main()
+{
+  /* Do stuff.  */
+  /* ... */
+
+  /* Must be called at the end of the test.  */
+  memmodel_done();
+
+  return 0;
+}
Index: g++.dg/memmodel/guality.h
===================================================================
--- g++.dg/memmodel/guality.h	(revision 0)
+++ g++.dg/memmodel/guality.h	(revision 0)
@@ -0,0 +1 @@ 
+#include "../../gcc.dg/guality/guality.h"
Index: g++.dg/memmodel/memmodel.h
===================================================================
--- g++.dg/memmodel/memmodel.h	(revision 0)
+++ g++.dg/memmodel/memmodel.h	(revision 0)
@@ -0,0 +1 @@ 
+#include "../../gcc.dg/memmodel/memmodel.h"
Index: g++.dg/memmodel/memmodel.gdb
===================================================================
--- g++.dg/memmodel/memmodel.gdb	(revision 0)
+++ g++.dg/memmodel/memmodel.gdb	(revision 0)
@@ -0,0 +1 @@ 
+source ../../gcc.dg/memmodel/memmodel.gdb
Index: g++.dg/memmodel/memmodel.exp
===================================================================
--- g++.dg/memmodel/memmodel.exp	(revision 0)
+++ g++.dg/memmodel/memmodel.exp	(revision 0)
@@ -0,0 +1,49 @@ 
+# Your run of the mill dg test, but verify that we have a working GDB first.
+
+load_lib g++-dg.exp
+load_lib gcc-memmodel-gdb-test.exp
+
+proc check_guality {args} {
+    set result [eval check_compile guality_check executable $args "-g -O0"]
+    set lines [lindex $result 0]
+    set output [lindex $result 1]
+    set ret 0
+    if {[string match "" $lines]} {
+      set execout [g++_load "./$output"]
+      set ret [string match "*1 PASS, 0 FAIL, 0 UNRESOLVED*" $execout]
+    }
+    remote_file build delete $output
+    return $ret
+}
+
+dg-init
+
+# Test the presence of gdb with the guality infrastructure.
+global GDB
+if ![info exists ::env(GUALITY_GDB_NAME)] {
+    if [info exists GDB] {
+	set guality_gdb_name "$GDB"
+    } else {
+	set guality_gdb_name "[transform gdb]"
+    }
+    setenv GUALITY_GDB_NAME "$guality_gdb_name"
+}
+if {[check_guality "
+  #include \"$srcdir/$subdir/guality.h\"
+  volatile long int varl = 6;
+  int main (int argc, char *argv\[\])
+  {
+    GUALCHKVAL (varl);
+    return 0;
+  }
+"]} {
+  dg-runtest [lsort [glob $srcdir/$subdir/*.C]] "-g" ""
+# Uncomment line below when we have common C/C++ tests.
+#  dg-runtest [lsort [glob $srcdir/c-c++-common/memmodel/*.c]] "-g" ""
+}
+
+if [info exists guality_gdb_name] {
+    unsetenv GUALITY_GDB_NAME
+}
+
+dg-finish
Index: g++.dg/memmodel/atomics-1.C
===================================================================
--- g++.dg/memmodel/atomics-1.C	(revision 0)
+++ g++.dg/memmodel/atomics-1.C	(revision 0)
@@ -0,0 +1,66 @@ 
+/* { dg-do link } */
+/* { dg-options "-std=c++0x -O2" } */
+/* { dg-final { memmodel-gdb-test } } */
+
+/* Test that atomic int and atomic char work properly.  */
+
+using namespace std;
+
+#include <atomic>
+#include <limits.h>
+#include <stdio.h>
+#include "memmodel.h"
+
+atomic<int> atomi;
+atomic<char> atomc;
+
+/* No need for parallel threads to do anything */
+void memmodel_other_threads()
+{
+}
+
+/* Verify after every instruction is executed, that the atmoic int and
+   char have one of the 2 legitimate values. */
+int memmodel_step_verify()
+{
+  if (atomi != 0 && atomi != INT_MAX)
+    {
+      printf ("FAIL: invalid intermediate result for atomi (%d).\n",
+	      (int)atomi);
+      return 1;
+    }
+  if (atomc != 0 && atomc != CHAR_MAX)
+    {
+      printf ("FAIL: invalid intermediate result for atomc (%d).\n",
+	      (int)atomc);
+      return 1;
+    }
+  return 0;
+}
+
+
+/* Verify that both atmoics have the corerct value.  */
+int memmodel_final_verify()
+{
+  if (atomi != INT_MAX)
+    {
+      printf ("FAIL: invalid final result for atomi (%d).\n",
+	      (int)atomi);
+      return 1;
+    }
+  if (atomc != CHAR_MAX)
+    {
+      printf ("FAIL: invalid final result for atomc (%d).\n",
+	      (int)atomc);
+      return 1;
+    }
+  return 0;
+}
+
+/* Test a store to an atomic int and an atomic char. */
+main()
+{
+  atomi = INT_MAX;
+  atomc = CHAR_MAX;
+  memmodel_done();
+}