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