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

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.

> 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