<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"><<a href="mailto:matthias@ccs.neu.edu" target="_blank">matthias@ccs.neu.edu</a>></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>
(--> [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 <<a href="mailto:monica.tomson@gmail.com">monica.tomson@gmail.com</a>> wrote:<br>
<br>
> Ahhh!! Your suggestion really simplifies and cleans up my original model!<br>
><br>
> Thanks :-)<br>
><br>
><br>
><br>
> On Mon, Jul 15, 2013 at 12:26 PM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> wrote:<br>
><br>
> I don't think you need 'dots' for what you want.<br>
><br>
> Here is how you can organize your states:<br>
> n -- name of current thread<br>
> C -- control of current thread<br>
> E -- env of current thread<br>
> S -- global store<br>
> K -- continuation of current thread<br>
> T -- thread pool : Name |-->f <C E K> (a finite map from names to states)<br>
><br>
> Then your beta-value reduction works as normal on the registers C through K and you can keep n and T opaque.<br>
><br>
> Thread switches swap in/out the relevant C E Ks.<br>
><br>
> No ellipses needed to single out the current thread.<br>
><br>
><br>
><br>
> On Jul 15, 2013, at 12:40 PM, Monica Tomson <<a href="mailto:monica.tomson@gmail.com">monica.tomson@gmail.com</a>> wrote:<br>
><br>
> ><br>
> ><br>
> ><br>
> > On Mon, Jul 15, 2013 at 6:48 AM, Matthias Felleisen <<a href="mailto:matthias@ccs.neu.edu">matthias@ccs.neu.edu</a>> wrote:<br>
> ><br>
> > 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>
> ><br>
> > Yeah. the machine is a CESK machine, and the reduction rule is function application essentially.<br>
> ><br>
> > The change is that I want to model thread spawn and join,<br>
> > which I think I can remodel the whole machine in the way that I can still "plug" the previous rules, except join and spawn, which i need to write new). and So, the model with thread is:<br>
> ><br>
> > (context (M å ê))<br>
> > (thread (tid context) )<br>
> > (threads (thread ...))<br>
> ><br>
> > at the same time using a global store (Store) for simplicity, but really a state is a threads * store<br>
> ><br>
> > and for the reduction with syntax error reported in the previous rule,<br>
> > (Some mistakes in the original post, so I copy-past it again below),<br>
> > I try to use pattern matching the treads list, which tries to get the first thread entry from the list of threads,<br>
> ><br>
> > (--><br>
> > (((tid (V å (fn ((ë X M) å_f) ê))) ...) S) ; tid, context<br>
> > (((tid (M (update å_f X ó_n) ê)) ...) S)<br>
> > tcesk3<br>
> > (where ó_n ,(fresh-ó))<br>
> > (side-condition<br>
> > (not (redex-match thread-cesk-iswim-plus X (term V ))) ) ;syntax: missing ellipsis with pattern variable in template in: V<br>
> > (side-condition<br>
> > (begin (store-update! (term ó_n) (term (V å)) Store) #t)))<br>
> ><br>
> > 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>
> ><br>
> > Thanks,<br>
> > --Monica<br>
> ><br>
> ><br>
> ><br>
> > On Jul 15, 2013, at 4:28 AM, Monica Tomson wrote:<br>
> ><br>
> > > Hi,<br>
> > ><br>
> > > I have the following reduction rule, it keeps on throwing the compiling error:missing ellipsis with pattern variable in template in: V<br>
> > ><br>
> > > I am confused where to put the ellipsis?<br>
> > ><br>
> > ><br>
> > > (--> ;((V å) S (fn ((ë X M) å_f) ê))<br>
> > > ;((M (update å_f X ó_n)) S ê)<br>
> > > ((tid (V å (fn ((ë X M) å_f) ê))) ...) ; tid, context<br>
> > > ((tid (M (update å_f X ó_n) ê)) ...)<br>
> > > tcesk3<br>
> > > (where ó_n ,(fresh-ó))<br>
> > > (side-condition<br>
> > > (not (redex-match thread-cesk-iswim-plus X (term V ))) ) ; ERROR: syntax: missing ellipsis with pattern variable in template in: V<br>
> > > (side-condition<br>
> > > (begin (store-update! (term ó_n) (term (V å)) Store) #t)))<br>
> > ><br>
> > > Thanks,<br>
> > ><br>
> > > --Shuying<br>
> > > ____________________<br>
> > > Racket Users list:<br>
> > > <a href="http://lists.racket-lang.org/users" target="_blank">http://lists.racket-lang.org/users</a><br>
> ><br>
> ><br>
><br>
><br>
><br>
><br>
> --<br>
> Monica<br>
<br>
</div></div></blockquote></div><br><br clear="all"><div><br></div>-- <br><div dir="ltr">Monica</div>
</div></div>