You're absolutely right that the stuff about names of allocated locations was, and is, accidental complexity. In our FHPC '13 paper, it was particularly bad -- the business with renaming locations leaked into the language semantics itself. It got a little less awful with our POPL paper, where we just decided that our language would be quasi-deterministic modulo a permutation on location names. If you look at the technical report that goes with our POPL paper (not that I really recommend you do), there's an ugly little cluster of lemmas in the middle of the quasi-determinism proof that are basically there entirely because of name-related bookkeeping. So, for my dissertation (and because we're planning to do a journal paper), I (with a lot of advice from Neel) am refactoring that proof to make it much less nasty.*
It wouldn't be the first time that someone had to do a lot of name-related bookkeeping to deal with allocation -- what we do is actually kind of like what Neel did in his "FRP without Spacetime Leaks"
paper (see the paragraph on "Supportedness and Location Permutations"). Some other authors deal with this by just not doing allocation at all -- instead, they have a pre-existing, arbitrarily large store of locations where every location has some default initial value. That's how it is done in, for example, the Featherweight CnC language in the Concurrent Collections paper
that was the original model for how to structure our determinism proof. Note that there's no way to allocate a new location in the store in Featherweight CnC -- you don't need to, because they all already exist! In retrospect, it seems like that would have been a smart way for us to design our formalism. On the other hand, when one is programming with our Haskell library then one really does have to create and allocate new LVars, and so I suppose it's nice to have something in the formalism that corresponds to that.
The connection with distributed computing hasn't really done anything to change our approach to allocation and naming. The "Conflict-free replicated data types"
paper, for instance, ignores the question of how to create new replicas (and what to name them), and just assumes that there's a finite set of processes with one replica at each process. So we inherit that assumption in our own work.
(Thanks for asking, by the way! Maybe I should say a little more about all this stuff in my diss -- I didn't know anyone cared. :) )
* Incidentally, I've also updated the formalism to allow not only the usual least-upper-bound writes, but also any write that is both inflationary and commutative. (My dissertation, and the eventual journal paper, will cover this in much more detail.) So I would need to revisit the proof anyway, even if it weren't for this refactoring that we are doing.Edited at 2014-08-14 09:45 am (UTC)