Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!zaphod.mps.ohio-state.edu!swrinde!elroy.jpl.nasa.gov!decwrl!deccrl!news.crl.dec.com!herlihy
From: herlihy@crl.dec.com (Maurice Herlihy)
Newsgroups: comp.sys.encore
Subject: Sequential Consistency?
Message-ID: <1991Jun4.210114.11355@crl.dec.com>
Date: 4 Jun 91 21:01:14 GMT
Sender: news@crl.dec.com (USENET News System)
Organization: DEC Cambridge Research Lab
Lines: 62

Is the Multimax memory sequentially consistent?  (I.e., do reads and writes to memory occur in the order requested?)  In the course of tracking down strange behavior in an experimental mutual exclusion protocol, I wrote the following simple memory exerciser (code at the end of the message).

Processes P_0 and P_1 share a two-element buffer, initially [0,0].  The
processes enter a loop.  On the k-th iteration, process P_i writes k to slot i
and reads the other slot.  It is an easy case analysis to show that if P_i and
P_j respectively read v_i and v_j on round k, then one or both of v_i and v_j
must be greater than or equal to k, provided the memory is sequentially consistent.

Every few million iterations, however, this property fails.  I wrote the
exerciser in C both using explicit system calls (proc_fork, share_malloc, etc.), and using the C parallel extensions (shared volatile declarations, etc.).  The assembly language listings from the C compiler don't show any reordering.

Any enlightenment would be greatly appreciated.

	Maurice Herlihy

-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
/*
  
  sequential consistency checker
  
  */

#include <parallel.h>

#define TEST_LENGTH 1024*1024

main() {
  int i, j, k;
  int *buffer, *log_0, *log_1, *log_i, *log_j;

  /* allocate shared data structures */
  share_malloc_init(4 * TEST_LENGTH * sizeof(int));
  buffer = (int*) share_malloc(2 * sizeof(int));
  log_0 = (int*) share_malloc(TEST_LENGTH * sizeof(int));
  log_1 = (int*) share_malloc(TEST_LENGTH * sizeof(int));
  
  /* initialze shared data structures */
  for (k = 0; k < TEST_LENGTH; k++){
    log_0[k] = 0;
    log_1[k] = 0;
  };
  buffer[0] = 0;
  buffer[1] = 0;

  /* start processes */
  i = proc_fork(2);		/* i is my process id */
  j = i ? 0 : 1;		/* j is the other's process id */
  log_i = i ? log_1 : log_0;	/* log_i is my log array */
  log_j = j ? log_1 : log_0;	/* log_j is the other's log array */
  for (k = 0; k < TEST_LENGTH; k++){
    buffer[i] = k;		/* write my slot */
    log_i[k] = buffer[j];	/* read and record other's slot */
  }
  proc_join();

  /* check for inconsistencies */
  for (k = 0; k < TEST_LENGTH; k++){
    if (log_0[k] < k && log_1[k] < k)
      printf("log_0[%d] = %d \t log_1[%d] = %d\n",
	     k, log_0[k], k, log_1[k]);
  }
}