[racket] Does Redex have support for multi-hole evaluation contexts?

On Sun, Jul 8, 2012 at 1:22 PM, Lindsey Kuper <lkuper at cs.indiana.edu> wrote:
> On Sun, Jul 8, 2012 at 9:30 AM, Robby Findler
> <robby at eecs.northwestern.edu> wrote:
>> Are there places where one side might do some effect that should be
>> visible by the other one? If so, then I guess that you must have some
>> way to identify those points so you make sure you cover all of the
>> possible interleavings?
>
> Yes.  Separate subcomputations can side-effect a store that other
> subcomputations can read.
>
>> I ask because it occurs to me that you could have an explicit token
>> that says whose turn it is an then use that to remove states from the
>> model. Whatever technique you're using to handle the above should also
>> be able to be adapted to this kind of explicit token thing. (Also, the
>> "token" could be something like "first one in a sequence" reduces and
>> then you could have a non-deterministic step that would pick the guy
>> that gets to go next. This would reduce the irrelevant interleaving,
>> possibly.)
>
> Having an explicit token that all "threads" could read would be
> another synchronization mechanism, wouldn't it?
>
> Of course, so is our notion of simultaneous forced steps that Ryan
> mentioned.  It would just be nice to be able to get away without one.

Well, perhaps this is already clear, but then I think that you're
probably missing important behavior if you force things to be in
lockstep. In particular, a real machine will probably let you do two
assignments in one thread (in a begin or something) between two other
assignments that happen in a parallel thread.

>> Also, I'm kind of sad but not surprised to hear that Redex's
>> performance is what motivates all this. If you'd like, please pass
>> along some program (and instructions for running it that makes it do
>> something slow) and I'll have a look to see if there is something
>> stupid going on and there is some straightforward improvement to Redex
>> that'd help out.
>
> That would be fanstastic, Robby!  Thanks!  I'll email you off-list with it.
>
> Lindsey