/*
 * Models the lock protocol used for concurrent access to B*-trees.
 * Based on one of the algorithms presented by Bayer and Schkolnick
 * in "Concurrency of Operation on B-Trees", Acta Informatica, 
 * Vol. 9, 1977, Springer-Verlag, pp. 1-21.
 * Wrote by Radu Iosif <iosif@athena.polito.it> Sun Apr 25 15:35:18 GMT 1999 
 */

#define K        2   /* B-tree order (2*k) */
#define MAXSLOT  4   /* MAXSLOT = K + 2 */

#define DEPTH    3   /* B-tree maximum depth */
#define MAXLOCK  4   /* MAXLOCK = DEPTH + 1 */

#define LOCK(n)      n.lock ? 0
#define UNLOCK(n)    n.lock ! 0


typedef node;

typedef slot {
  int key;
  node &ptr;
};


typedef node {
  chan lock = [1] of { bit };

  int  nslot;
  slot svect[MAXSLOT];

  int level;

  node &upper;
};


typedef nptr {
  node &ptr;
};


typedef lset {
  int nlock;
  nptr lvect[MAXLOCK];
};


node &root;


function b_init()
{
  root = new node;
  UNLOCK(root);
}


function set_add(node &n; lset &s)
{
#if 0
  assert(s != null);
  assert(n != null);
  assert(len(n.lock) == 0);
#endif

  s.nlock ++;
  s.lvect[s.nlock - 1].ptr = n;
}


function set_del(node &n; lset &s)
{
  int i;

#if 0
  assert(n != null);
  assert(s != null);
#endif

  do
  :: i < s.nlock
	-> if
	   :: s.lvect[i].ptr == n
		-> do
                   :: i < s.nlock - 1
			-> s.lvect[i].ptr = s.lvect[i + 1].ptr;
			   i ++;

		   :: i == s.nlock - 1
			-> break;
	           od;
	
	           s.nlock --;
		   break;

	   :: else
		-> i ++;
	   fi;

  :: i == s.nlock
	-> break;
  od
}


function set_rel(lset &s)
{
#if 0
  assert(s != null);
#endif

  do
  :: s.nlock > 0 
	-> UNLOCK(s.lvect[s.nlock - 1].ptr);
       	   s.nlock --;

  :: s.nlock == 0
	-> break;
  od
}


function is_safe(node &n; lset &s)
{
  if
  :: n.nslot < K
        -> set_rel(s);
  :: else
	-> skip;
  fi;
}


function b_search(int key; node &n; lset &s) : node&
{
  int i;

#if 0
  assert(n != null);
  assert(s != null);
#endif

  if
  :: n.nslot == 0 
	-> set_add(n, s);
	   return n;
  :: else 
	-> skip;
  fi;

  do
  :: if 
     :: i == n.nslot
	  -> if
	     :: n.svect[i].ptr != null
		 -> LOCK(n.svect[i].ptr);
		    is_safe(n, s);
                    set_add(n, s);
		    return b_search(key, n.svect[i].ptr, s);

             :: else
	         ->  set_add(n, s);
		     return n;
             fi

     :: i < n.nslot
	  -> if
	     :: key > n.svect[i].key
		 -> i ++;

             :: else
		 -> if
                    :: n.svect[i].ptr != null
			-> LOCK(n.svect[i].ptr);
			   is_safe(n, s);
                           set_add(n, s);
			   return b_search(key, n.svect[i].ptr, s);

                    :: else
                        -> set_add(n, s);
	                   return n;
                    fi
             fi
     fi
   od;
}


function i_key(int key; node &n) : int
{
  int i, j;

#if 0
  assert(n != null);
#endif

  do
  :: if
     :: i == n.nslot 
	  -> break;

     :: else 
	  -> if
	     :: key > n.svect[i].key 
	          -> i ++;

             :: else 
                  -> break;
             fi
     fi
  od;

  j = n.nslot;

  do
  :: if
     :: i == j 
	  -> break;

     :: else
	  -> n.svect[j].key = n.svect[j - 1].key;
             n.svect[j].ptr = n.svect[j - 1].ptr;
             j --;
     fi
  od;

  n.svect[i].key = key;
  n.nslot ++;

  return i;
}


function b_expand(node &n; lset &s)
{
  node &lft, &rgt, &up;
  int i, Nslot;

#if 0
  assert(n != null);
#endif

  Nslot = n.nslot;

  if
  :: n.nslot > K
        -> if
	   :: n.upper == null 
		 -> up = new node;
	            up.level = n.level + 1;
                    n.upper = up;
                    set_add(up, s);
	            root = up;

           :: else 
	         -> up = n.upper;
           fi;

#if 0
           assert(len(up.lock) == 0);
#endif

	   lft = new node;
           lft.nslot = K / 2;

	   rgt = new node;
	   rgt.nslot = K / 2;

	   do
	   :: i <= Nslot / 2
		-> lft.svect[i].key = n.svect[i].key;
		   lft.svect[i].ptr = n.svect[i].ptr;

		   if
                   :: lft.svect[i].ptr != null
			-> lft.svect[i].ptr.upper = lft;
		   :: else
			-> skip;
		   fi;

	           rgt.svect[i].key = n.svect[i + K / 2 + 1].key;
	           rgt.svect[i].ptr = n.svect[i + K / 2 + 1].ptr;

		   if
		   :: rgt.svect[i].ptr != null
			-> rgt.svect[i].ptr.upper = rgt;
		   :: else
			-> skip;
		   fi;

		   i ++;

	   :: i > Nslot / 2
	        -> break;
	   od;

	   i = i_key(n.svect[K / 2].key, up);           

	   up.svect[i].ptr = lft;
	   up.svect[i + 1].ptr = rgt;

           lft.upper = up;
	   rgt.upper = up;

	   UNLOCK(lft);
	   UNLOCK(rgt);

	   set_del(n, s);
	   delete(n);

	   b_expand(up, s);

  :: else 
        -> skip;
  fi;
}


function b_insert(int key) : int
{
  node &n;
  lset &s;

  LOCK(root);

  if
  :: root.level == DEPTH - 1
	-> UNLOCK(root);
	   return 1;

  :: else
	-> s = new lset;
	   n = b_search(key, root, s);  
	   i_key(key, n);
	   b_expand(n, s);
	   set_rel(s);
	   delete(s);
           return 0;
  fi
}


proctype updater()
{
  int stop;

  do
  :: stop = b_insert(1) ->
	if
	:: stop -> break;
	:: else -> skip;
    	fi;
  od;
}


init {
  b_init();

  atomic {
    run updater();
    run updater();
  }
}