On Sun, Jul 8, 2012 at 1:22 PM, Lindsey Kuper <lku...@cs.indiana.edu> wrote: > On Sun, Jul 8, 2012 at 9:30 AM, Robby Findler > <ro...@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 ____________________ Racket Users list: http://lists.racket-lang.org/users
