1/* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 6 * See "LICENSE_BSD2.txt" for details. 7 * 8 * @TAG(NICTA_BSD) 9 */ 10 11#ifndef COMPILE 12#define NULL ((void*)0) 13#endif 14 15struct node { 16 struct node *l, *r; 17 unsigned m, c; 18}; 19 20/* This is Mehta & Nipkow's version of the algorithm (HOL/Hoare/SchorrWaite.thy). */ 21void schorr_waite(struct node *root) { 22 struct node *t = root, *p = NULL, *q; 23 while (p != NULL || (t != NULL && !t->m)) { 24 if (t == NULL || t->m) { 25 if (p->c) { 26 q = t; t = p; p = p->r; t->r = q; 27 } else { 28 q = t; t = p->r; p->r = p->l; p->l = q; p->c = 1; 29 } 30 } else { 31 q = p; p = t; t = t->l; p->l = q; p->m = 1; p->c = 0; 32 } 33 } 34} 35 36 37/* 38 * An executable specification for graph traversal. 39 */ 40void simple_traverse(struct node *n) { 41 if (n == NULL || n->m) { 42 return; 43 } 44 45 n->m = 1; 46 simple_traverse(n->l); 47 simple_traverse(n->r); 48} 49 50#ifdef COMPILE 51#include <stdlib.h> 52#include <assert.h> 53#include <sys/time.h> 54#include <time.h> 55 56void make_graph(unsigned size, unsigned graph[size][2], struct node n[size]) { 57 for (unsigned i = 0; i < size; ++i) { 58 if (graph[i][0] == size) { 59 n[i].l = NULL; 60 } else { 61 n[i].l = &n[0] + graph[i][0]; 62 } 63 if (graph[i][1] == size) { 64 n[i].r = NULL; 65 } else { 66 n[i].r = &n[0] + graph[i][1]; 67 } 68 n[i].c = n[i].m = 0; 69 } 70} 71 72int main(void) { 73 const unsigned max_size = 1000; 74 unsigned graph[max_size][2]; 75 76 struct timeval tv; 77 if (gettimeofday(&tv, NULL)) { 78 return 1; 79 } 80 unsigned long long t = (unsigned long long)tv.tv_sec * 1000000 + tv.tv_usec; 81 const int seed = (t >> 32) ^ t; 82 83 srand(seed); 84 unsigned size = rand() % max_size + 1; 85 for (unsigned i = 0; i < size; ++i) { 86 graph[i][0] = rand() % (size+1); 87 graph[i][1] = rand() % (size+1); 88 } 89 90 struct node n1[max_size], n2[max_size]; 91 make_graph(size, graph, n1); 92 make_graph(size, graph, n2); 93 94 schorr_waite(n1); 95 simple_traverse(n2); 96 97 for (unsigned i = 0; i < size; ++i) { 98 if (graph[i][0] == size) { 99 assert(n1[i].l == NULL); 100 assert(n2[i].l == NULL); 101 } else { 102 assert(n1[i].l == n1 + graph[i][0]); 103 assert(n2[i].l == n2 + graph[i][0]); 104 } 105 if (graph[i][1] == size) { 106 assert(n1[i].r == NULL); 107 assert(n2[i].r == NULL); 108 } else { 109 assert(n1[i].r == n1 + graph[i][1]); 110 assert(n2[i].r == n2 + graph[i][1]); 111 } 112 assert(n1[i].m == n2[i].m); 113 } 114 115 return 0; 116} 117#endif 118