1#lang racket 2(require redex) 3 4#| 5 6semaphores make things much more predictable... 7 8|# 9 10(reduction-steps-cutoff 100) 11 12(define-language lang 13 (p ((store (variable v) ...) 14 (semas (variable sema-count) ...) 15 (threads e ...))) 16 (sema-count number 17 none) 18 (e (set! variable e) 19 (begin e ...) 20 (semaphore variable) 21 (semaphore-wait e) 22 (semaphore-post e) 23 (lambda (variable) e) 24 (e e) 25 variable 26 (list e ...) 27 (cons e e) 28 number 29 (void)) 30 (p-ctxt ((store (variable v) ...) 31 (semas (variable sema-count) ...) 32 (threads e ... e-ctxt e ...))) 33 (e-ctxt (e-ctxt e) 34 (v e-ctxt) 35 (cons e-ctxt e) 36 (cons v e-ctxt) 37 (list v ... e-ctxt e ...) 38 (set! variable e-ctxt) 39 (begin e-ctxt e ...) 40 (semaphore-wait e-ctxt) 41 (semaphore-post e-ctxt) 42 hole) 43 (v (semaphore variable) 44 (lambda (variable) e) 45 (list v ...) 46 number 47 (void))) 48 49(define reductions 50 (reduction-relation 51 lang 52 (--> (in-hole (name c p-ctxt) (begin v e_1 e_2 e_rest ...)) 53 (in-hole c (begin e_1 e_2 e_rest ...))) 54 (--> (in-hole (name c p-ctxt) (cons v_1 (list v_2s ...))) 55 (in-hole c (list v_1 v_2s ...))) 56 (--> (in-hole (name c p-ctxt) (begin v e_1)) 57 (in-hole c e_1)) 58 (--> (in-hole (name c p-ctxt) (begin v_1)) 59 (in-hole c v_1)) 60 (--> ((store 61 (variable_before v_before) ... 62 ((name x variable) (name v v)) 63 (variable_after v_after) ...) 64 (name semas any) 65 (threads 66 e_before ... 67 (in-hole (name c e-ctxt) (name x variable)) 68 e_after ...)) 69 ((store 70 (variable_before v_before) ... 71 (x v) 72 (variable_after v_after) ...) 73 semas 74 (threads 75 e_before ... 76 (in-hole c v) 77 e_after ...))) 78 (--> ((store (variable_before v_before) ... 79 (variable_i v) 80 (variable_after v_after) ...) 81 (name semas any) 82 (threads 83 e_before ... 84 (in-hole (name c e-ctxt) (set! variable_i v_new)) 85 e_after ...)) 86 ((store (variable_before v_before) ... 87 (variable_i v_new) 88 (variable_after v_after) ...) 89 semas 90 (threads 91 e_before ... 92 (in-hole c (void)) 93 e_after ...))) 94 (--> ((name store any) 95 (semas 96 (variable_before v_before) ... 97 (variable_sema number_n) 98 (variable_after v_after) ...) 99 (threads 100 e_before ... 101 (in-hole (name c e-ctxt) (semaphore-wait (semaphore variable_sema))) 102 e_after ...)) 103 (store 104 (semas 105 (variable_before v_before) ... 106 (variable_sema ,(if (= (term number_n) 1) 107 (term none) 108 (- (term number_n) 1))) 109 (variable_after v_after) ...) 110 (threads 111 e_before ... 112 (in-hole c (void)) 113 e_after ...))) 114 (--> ((name store any) 115 (semas 116 (variable_before v_before) ... 117 (variable_sema number_n) 118 (variable_after v_after) ...) 119 (threads 120 e_before ... 121 (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) 122 e_after ...)) 123 (store 124 (semas 125 (variable_before v_before) ... 126 (variable_sema ,(+ (term number_n) 1)) 127 (variable_after v_after) ...) 128 (threads 129 e_before ... 130 (in-hole c (void)) 131 e_after ...))) 132 133 (--> ((name store any) 134 (semas 135 (variable_before v_before) ... 136 (variable_sema none) 137 (variable_after v_after) ...) 138 (threads 139 e_before ... 140 (in-hole (name c e-ctxt) (semaphore-post (semaphore variable_sema))) 141 e_after ...)) 142 (store 143 (semas 144 (variable_before v_before) ... 145 (variable_sema 1) 146 (variable_after v_after) ...) 147 (threads 148 e_before ... 149 (in-hole c (void)) 150 e_after ...))))) 151 152(stepper reductions 153 `((store (y (list))) 154 (semas) 155 (threads (set! y (cons 1 y)) 156 (set! y (cons 2 y))))) 157 158(stepper reductions 159 `((store (y (list))) 160 (semas (x 1)) 161 (threads (begin (semaphore-wait (semaphore x)) 162 (set! y (cons 1 y)) 163 (semaphore-post (semaphore x))) 164 (begin (semaphore-wait (semaphore x)) 165 (set! y (cons 2 y)) 166 (semaphore-post (semaphore x)))))) 167