Simonpj/Talk:LwConc

Talk page for "Lightweight concurrency primitives for GHC"

This is a discussion page for the paper Lightweight concurrency primitives for GHC.

If you are kind enough to read this paper, you may like to jot down any thoughts it triggers off, and see what others have written. This talk-page lets you do just that.

You can identify your entries by preceding them with four tildes. Doing so adds your name, and the date. Thus:

Simonpj 08:42, 19 April 2007 (UTC) Note from Simon

If you say who you are in this way, we'll be able to acknowledge your help in a revised version of the paper.

---

With regards to the semantics of PTM exception handling (PAtomicExp, PCatchExp) I initially wondered why the definition of the heap after the transition :$\Theta \cup (\Theta '\setminus \Theta )$ was not the simpler, equivalent expression: $\Theta \cup \Theta '$. I stopped wondering when I read that the set difference was meant as a domain restriction thus $\Theta \cup \Theta '|_{dom(\Theta ')-dom(\Theta )}$. Which makes sense with respect to the semantics of handling the thrown exception, but perhaps this should be reflected in the notation. This got me thinking a bit more about the semantics.

"Composable memory transactions" (Harris, Marlow, Peyton Jones, Herlihy, 2005) is referenced in explanation of retaining the allocated PVars when an exception is thrown. The paper includes the slightly different STM semantics in which $\Delta$ is built as redundant record of allocation effects (when newTVar is applied). When an exception is thrown the resulting heap is $\Theta \cup \Delta '$, therefore we return to the heap state before the application, with allocation *only* effects remaining intact.

However in the PTM semantics there is no allocation effects store and (as mentioned above) the heap state resulting from a thrown exception is the union of the initial heap state and the domain restricted final heap state. Surely this can then include more than just allocation effects, but effects of PVar writes if writePVar is applied?

For example, if there is a heap, $\Theta =\{a\mapsto M1\}$ and we apply:

  atomicPTM $ do
      b <- newPVar M2
      writePVar b M3
      throw .....

Our heap at the time of throw (as far as I understand) would be $\Theta '=\{a\mapsto M1,b\mapsto M3\}.$ Therefore from the PAtomicExp rule the resulting heap, $\Theta \cup \Theta '|_{dom(\Theta ')-dom(\Theta )}$, is also $\{a\mapsto M1,b\mapsto M3\}$. The effect of the writePVar comes through.

If only allocation effects were preserved the resultant heap should be $\{a\mapsto M1,b\mapsto M2\}$.

Surely it is our aim to undo the write effects here as in the STM semantics? Perhaps to correct this the allocation effects set as seen in STM could be introduced. Alternatively, I have misunderstood some crucial points and I apologise! Thanks.

Dorchard 19:06, 11 February 2008 (UTC)