Example showing problem with current isolation semantics in CDL

Hi

After the recent discussion on isolation being inherited from the enclosing choreography, I wanted to outline the following example to show how simply changing the isolation attribute of an enclosing choreography can significantly change the behavior of the choreography.

<choreo A>
    <variable name="var1" /> 
    <variable name="var2" />
    <choreo B isolation=true >
        <assign value "x" to "var1" /> 
        <assign value "x" to "var2" />
    </choreo>
    <choreo C isolation=true > 
        <assign value "y" to "var1" /> 
        <assign value "y" to "var2" />
    </choreo>

    <parallel>
        <perform choreo B>
             <bind var1/>
             <bind var2/>
        </perform>
        <perform choreo C>
             <bind var1/>
             <bind var2/>
        </perform>
    </parallel>
</choreo>

If choreo A is not isolated, then choreo B and C are isolated in their own right - and therefore because they are both accessing common variables, I assume that one or the other of the performs will wait until the other has completed - so in fact they will be performed in sequence. [If this assumption is not true, then I need to have an explanation of the behavior when two sub-choreos have the same isolated variable - at what point do they wait?]

Therefore the result would be that both variables would have the same value - either 'x' or 'y' depending on the order in which the sub-choreos were actually performed.

However, if we now make choreo A isolated, the isolated attribute on B and C is now ignored, as the isolation is inherited from the parent choreography (as described at the last f2f).

This now means that because the variables 'var1' and 'var2' are within the same isolation scope, when the two sub-choreos are performed, there is no waiting/blocking. This means that the result of the overall choreography is non-deterministic, the variables could have any combination of 'x' or 'y'.

The problem is that a sub-choreography may be defined on the basis of having isolation semantics - and this is effectively overridden when performed from an already isolated choreography. Whereas if nested isolation was supported, the semantics of the sub-choreographies would be preserved, regardless of the isolation status of the enclosing choreography.

This example is showing a simple example, but in a real example the isolation of a top level choreography could have unforeseen consequences on a sub-choreography that is many levels of nesting removed from the isolated choreography. A case of a small change having a significant impact on bahavior.

Regards
Gary