This looks like a fairly conventional form of parallel evaluation with some form of attempt at 'free deterministic update'.
If I were to model this kind of thing, I am sure I'd use a multi-hole reduction semantics to represent non-coordinated parallelism. Too bad Redex can't model this, but it doesn't mean you can't formulate it as a plain old reduction semantics. Whether you "believe" it to be deterministic is pretty irrelevant. If you want it to be deterministic, you construct it that way, and with multi-hole "standard" reductions it is quite easy (near trivial) to show this -- assuming you get your effects right. Enough said, good luck -- Matthias On Jul 9, 2012, at 3:11 PM, Ryan Newton wrote: > Hi all, > > Thanks for all the advice. > > Just to be clear about the context. This is a parallel language that we > developed on paper which we strongly believed was deterministic. We wrote > the paper proof and also, on the side, wanted to make a redex model to check > ourselves. > > We felt it was necessary to include simultaneous steps (Matthias's [A] > scenario) to model real parallel machines and force us to deal with > potentially incompatible simultaneous updates to the store. > > Lindsey had a slightly awkward time shoehorning things into redex, and the > resulting model runs pretty slowly. BUT, these are just nits and possible > areas for improvement. Redex was still enormously helpful and fulfilled its > purpose. There wasn't any existential crisis here. > > -Ryan > > P.S. It would be simpler to just share the paper rather than describing the > problems out of context. However, I don't want to send the draft out quite > yet, because it needs a few more tweaks to have all the refactorings pushed > through and achieve internal consistency. But I'm attached the reduction > rules and grammar, FYI. > > On Mon, Jul 9, 2012 at 12:34 PM, Matthias Felleisen <matth...@ccs.neu.edu> > wrote: > > On Jul 9, 2012, at 6:29 AM, Lindsey Kuper wrote: > > > I had been assuming that "one-step" meant "small-step", but > > now I think that by "one-step" David means a relation that doesn't > > reduce redexes in parallel. So, in fact, ours *is* multi-step because > > it *does* reduce in parallel. > > > Lindsey and Ryan, I have had no time until now to catch up with this thread > (argh). And I have my own POPL deadline, so here are some general remarks: > > 1. The parallel reduction trick that David pointed out goes back to the early > 1970s. Tait appears to be the source. See Barendregt. > > 2. 'small step' is NOT 'one-step' and 'one-step' is not 'notion of > reduction'. See Redex, chapter 1 for definitions. They are the same ones as > Barendregt uses and the informed PL community has used when publishing > semantics papers in this style. I dislike 'small step' A LOT but if you want > a relationship |---> (standard reduction) is what most publishing PLists > would call a 'small step' semantics. > > 3. Also Redex, chapter 1 suggests that 'eval' is the actual semantics and > |---> or -->> are two distinct ways of specifying it. Since eval is the key, > this also eliminates any worries about reflexive rules -- as long as you > think of eval as the mathematical semantics and the arrow relations as just > one possible mechanism to define it. > > 4. The reduction relations (-->> or standard) become important only if you > wish to make some claim about the intension of the semantics, i.e., how it > relates to actual machine steps. You don't have to. Plotkin 74, for example, > shows that it is perfectly okay to show two different unrelated ways of > defining eval (secd and a recursive interpreter) and to prove them equivalent > -- brute force in his case. You do that because you might be able to use one > definitional mechanism to show one thing (type soundness) and with another > one you can show something else (cost of execution). I have done it many > times. > > 5. The confusion between reduction relations and parallel execution is about > 40 years old (perhaps a bit less). Indeed, the confusion between reduction > relations in LC and plain execution is that old -- see so-called "optimal > reduction sequences", which a well-trained computer scientist (===/== > mathematician masquerading as a PL person) will quickly recognize that it is > nonsense. Fortunately we have had a proof for 10 years that this horse is > dead. > > ;; --- > > May I propose a re-thinking of your approach that may benefit us Redex > designers? > > -- figure out what your real goal is; it cannot be to develop a semantics of > some hypothetical PL (see above, especially 4) > -- develop a paper and pencil model of a semantics that helps you prove this > goal/theorem > -- if it happens to be a reduction semantics (I am of course convinced that > 90% of all goals can be reached via reduction semantics), > allow one of two things to happen: > [A] you need to model 'simultaneous' steps meaning you need multi-hole > [B] you don't need truly simultaneous steps but you allow some > non-determinism in |---> > > For [A], Redex is ill-suited. The define-judgment form isn't remotely as > helpful for semantics as is the core redex language. > > For [B], Redex is your friend. > > See my paper with Cormac in the mid 90s on modeling futures with reduction > systems, for one approach to parallelism. We did intend to tackle an FP > language with set! at the time, but the analysis didn't work out so we > abandoned this direction. > > In short, decouple what you want to accomplish from the tool that might look > like it could help. > > > -- Matthias > > > ____________________ > Racket Users list: > http://lists.racket-lang.org/users > > <grammar_excerpt.pdf><semantics_excerpt.pdf> ____________________ Racket Users list: http://lists.racket-lang.org/users
