Added spin homework

Homework/Homework_4/incdec.c

+#include <pthread.h>
+#include <limits.h>
+
+// verify incdec.c # uses incdec.prx
+
+#define uint	unsigned int
+
+volatile uint value = 0;
+volatile uint inc_flag = 0;
+volatile uint dec_flag = 0;
+
+#ifndef MODEX
+#include <stdlib.h>
+#include <assert.h>
+void
+cas(volatile uint *v,
+    volatile uint  e,
+    volatile uint  u,
+    volatile uint *r,
+    volatile uint *flag)
+{
+	if (*v == e)
+	{	*flag = 1, *v = u, *r = 1;
+	} else
+	{	*r = 0;
+	}
+}
+#endif
+
+uint
+inc(void)
+{	uint inc_v, inc_vn, inc_casret;
+
+	do {
+		inc_v = value;
+		if (inc_v == UINT_MAX)
+		{	return 0;	// fail, return min
+		}
+		inc_vn = inc_v + 1;
+		cas(&value, inc_v, inc_vn, &inc_casret, &inc_flag);
+	} while (inc_casret==0);
+
+	assert(dec_flag || value > inc_v);
+
+	return inc_vn;
+}
+
+uint
+dec(void)
+{	uint dec_v, dec_vn, dec_casret;
+
+	do {
+		dec_v = value;
+		if (dec_v == 0)
+		{	return UINT_MAX; // fail, return max
+		}
+		dec_vn = dec_v - 1;
+		cas(&value, dec_v, dec_vn, &dec_casret, &dec_flag);
+	}
+	while (dec_casret==0);
+
+	assert(inc_flag || value < dec_v);
+
+	return dec_vn;
+}
+
+void *
+thread(void *arg)
+{	int r;
+
+	r = rand();
+
+	if (r)
+	{	inc();
+	} else
+	{	dec();
+	}
+
+	return 0;
+}
+
+int
+main(void)
+{	pthread_t t;
+
+	while(1) {
+		pthread_create(&t, 0, thread, 0);
+	}
+	exit(0);
+}

Homework/Homework_4/incdec.prx

+%X -xe2
+%C
+void
+cas(volatile uint *v,
+    volatile uint  e,
+    volatile uint  u,
+    volatile uint *r,
+    volatile uint *flag)
+{
+	if (*v == e)
+	{	*flag = 1, *v = u, *r = 1;
+	} else
+	{	*r = 0;
+	}
+}
+%L
+r=rand()	if :: r = 0 :: r = 1 fi

Homework/Homework_4/philo-1.pml

+#define N 5
+
+bit chopsticks[N];
+bit eats[N];
+
+init {
+  atomic {
+    byte i = 0;
+    do
+    ::(i < N) -> run philosopher(i); i++;
+    ::else -> break;
+    od;
+  }
+}
+
+proctype philosopher(byte id) {
+  eats[id] = 0;
+thinking:
+  atomic { chopsticks[id] == 0 -> chopsticks[id] = 1; }
+  atomic { chopsticks[(id + 1)%N] == 0; -> chopsticks[(id + 1)%N] = 1; }
+  eats[id] = 1;
+eating:
+  eats[id] = 0;
+  chopsticks[(id + 1)%N] = 0; 
+  chopsticks[id] = 0;
+  goto thinking;
+}
+
+ltl ltl_some {
+  [] <> (eats[0] || eats[1] || eats[2] || eats[3] || eats[4])
+}
+
+ltl ltl_two {
+  [] <> (eats[0] && eats[2])
+}

Homework/Homework_4/philo-2.c

+#include <pthread.h>
+#include <unistd.h>
+#include <assert.h>
+#include <stdlib.h>
+#include <stdio.h>
+
+#define N 5
+
+/* run with: verify philo-2.c */
+
+/* completely wrong: no mutexes / semaphors; deadlock */
+
+int eats[N];
+int chopsticks[N];
+
+void *philosopher(void *arg)
+{
+  int id, nextid;
+  
+  id = (long) arg;
+  nextid = (id + 1) % N;
+
+  eats[id] = 0;
+  
+  while (1) {
+    usleep(1000); /* think */
+    
+    while (chopsticks[id] == 1) usleep(10);
+    chopsticks[id] = 1;
+    while (chopsticks[nextid] == 1);
+    chopsticks[nextid] = 1;
+
+    eats[id]++;
+    usleep(1000); /* eat */
+    
+    chopsticks[id] = 0;
+    chopsticks[nextid] = 0;
+  }
+}
+
+int main(void)
+{
+  pthread_t t[N];
+  long i;
+  
+  for (i = 0; i < N; i++)
+    chopsticks[i] = eats[i] = 0;
+  
+  for (i = 0; i < N; i++)
+    pthread_create(&t[i], 0, philosopher, (void *) i);
+
+  usleep(1000000);
+  
+  for (i = 0; i < N; i++)
+    assert(eats[i] > 100);
+
+  return 0;
+}