<div dir="ltr"><br><div class="gmail_extra"><br><br><div class="gmail_quote">On Mon, Jul 15, 2013 at 1:31 PM, Matthias Felleisen <span dir="ltr">&lt;<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>&gt;</span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><br>
For thread swapping, consider<br>
<br>
(--&gt; [n C E S K {th_1 ... (n_i C_i E_i K_i) th_j ...}]<br>
     [n_i C_i E_i S K_i {th_1 ... (n C E K) th_j ...}])<br>
<br>
as a rule. This illustrates ellipses. The rule non-deterministically picks one of the threads to swap in and Redex can show you all branches.<br>
<br>
Alternative, rotate threads in and out.<br>
<br>
The above rule uses different kinds of parens to delimit pieces; this works in Redex.<br>
<br>
BTW, names are optional.<br>
<div class="HOEnZb"><div class="h5"><br><br></div></div></blockquote><div><br></div><div>Really useful! Good learning experience so far! </div><div> Appreciated! </div><div><br></div><div>Doing wait/notifyall now, in addition to the join/spawn. :)</div>
<div><br></div><div>Hopefully I can test out some simple cases when it is done..</div><div><br></div><div>Thanks again, </div><div>--Monica</div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="HOEnZb"><div class="h5">
On Jul 15, 2013, at 2:57 PM, Monica Tomson &lt;<a href="mailto:monica.tomson@gmail.com">monica.tomson@gmail.com</a>&gt; wrote:<br>
<br>
&gt; Ahhh!! Your suggestion really simplifies and cleans up my original model!<br>
&gt;<br>
&gt; Thanks :-)<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On Mon, Jul 15, 2013 at 12:26 PM, Matthias Felleisen &lt;<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>&gt; wrote:<br>
&gt;<br>
&gt; I don&#39;t think you need &#39;dots&#39; for what you want.<br>
&gt;<br>
&gt; Here is how you can organize your states:<br>
&gt;  n -- name of current thread<br>
&gt;  C -- control of current thread<br>
&gt;  E -- env of current thread<br>
&gt;  S -- global store<br>
&gt;  K -- continuation of current thread<br>
&gt;  T -- thread pool : Name |--&gt;f &lt;C E K&gt; (a finite map from names to states)<br>
&gt;<br>
&gt; Then your beta-value reduction works as normal on the registers C through K and you can keep n and T opaque.<br>
&gt;<br>
&gt; Thread switches swap in/out the relevant C E Ks.<br>
&gt;<br>
&gt; No ellipses needed to single out the current thread.<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On Jul 15, 2013, at 12:40 PM, Monica Tomson &lt;<a href="mailto:monica.tomson@gmail.com">monica.tomson@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; On Mon, Jul 15, 2013 at 6:48 AM, Matthias Felleisen &lt;<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>&gt; wrote:<br>
&gt; &gt;<br>
&gt; &gt; Is this supposed to be a CESK machine state where you apply \x.M to V (actually V and the empty env, which is a highly unusual left-hand side)?<br>
&gt; &gt;<br>
&gt; &gt; Yeah. the machine is a CESK machine, and the reduction rule is function application essentially.<br>
&gt; &gt;<br>
&gt; &gt; The change is that I want to model thread spawn and join,<br>
&gt; &gt; which I think I can remodel the whole machine  in the way  that I can still &quot;plug&quot; the previous rules, except join and spawn, which i need to write new). and So, the model with thread is:<br>
&gt; &gt;<br>
&gt; &gt;  (context (M å ê))<br>
&gt; &gt;  (thread (tid context) )<br>
&gt; &gt;  (threads  (thread ...))<br>
&gt; &gt;<br>
&gt; &gt; at the same time using a global store (Store) for simplicity, but really a state is a threads * store<br>
&gt; &gt;<br>
&gt; &gt; and for the reduction with syntax error reported in the previous rule,<br>
&gt; &gt;  (Some mistakes in  the original post, so I copy-past it again below),<br>
&gt; &gt; I try to use pattern matching the treads list, which tries to get the first thread entry from the list of threads,<br>
&gt; &gt;<br>
&gt; &gt; (--&gt;<br>
&gt; &gt;     (((tid   (V å (fn ((ë X M) å_f) ê))) ...) S) ; tid, context<br>
&gt; &gt;      (((tid  (M  (update å_f X ó_n) ê)) ...) S)<br>
&gt; &gt;      tcesk3<br>
&gt; &gt;      (where ó_n ,(fresh-ó))<br>
&gt; &gt;      (side-condition<br>
&gt; &gt;       (not (redex-match thread-cesk-iswim-plus X (term V ))) )  ;syntax: missing ellipsis with pattern variable in template in: V<br>
&gt; &gt;     (side-condition<br>
&gt; &gt;       (begin (store-update! (term ó_n) (term (V å)) Store) #t)))<br>
&gt; &gt;<br>
&gt; &gt; I am not sure the design or the whole things making sense or not, but just trying to do some exercise of using PLT-Redex...<br>
&gt; &gt;<br>
&gt; &gt; Thanks,<br>
&gt; &gt; --Monica<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt; &gt; On Jul 15, 2013, at 4:28 AM, Monica Tomson wrote:<br>
&gt; &gt;<br>
&gt; &gt; &gt; Hi,<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; I have the following reduction rule, it keeps on throwing the compiling error:missing ellipsis with pattern variable in template in: V<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; I am confused where to put the ellipsis?<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; (--&gt; ;((V å) S (fn ((ë X M) å_f) ê))<br>
&gt; &gt; &gt;         ;((M (update å_f X ó_n)) S ê)<br>
&gt; &gt; &gt;      ((tid  (V å (fn ((ë X M) å_f) ê))) ...) ; tid, context<br>
&gt; &gt; &gt;      ((tid  (M  (update å_f X ó_n) ê)) ...)<br>
&gt; &gt; &gt;      tcesk3<br>
&gt; &gt; &gt;      (where ó_n ,(fresh-ó))<br>
&gt; &gt; &gt;      (side-condition<br>
&gt; &gt; &gt;       (not (redex-match thread-cesk-iswim-plus X (term V ))) )  ; ERROR: syntax: missing ellipsis with pattern variable in template in: V<br>
&gt; &gt; &gt;     (side-condition<br>
&gt; &gt; &gt;       (begin (store-update! (term ó_n) (term (V å)) Store) #t)))<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; Thanks,<br>
&gt; &gt; &gt;<br>
&gt; &gt; &gt; --Shuying<br>
&gt; &gt; &gt; ____________________<br>
&gt; &gt; &gt;  Racket Users list:<br>
&gt; &gt; &gt;  <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
&gt; &gt;<br>
&gt; &gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; --<br>
&gt; Monica<br>
<br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr">Monica</div>
</div></div>