Operational semantics question

[p.kame...@gmail.com]

Hi,

I'm trying to implement a Ceu DSL in Haskell, but I'm stuck on understanding the exact operational semantics described in the paper "A Memory-Bounded, Deterministic and Terminating Semantics for the Synchronous Programming Language Céu".

For example, let's take the following program:

par/and do
    emit e;
  with
    await e;
    _printf("here");
end

To my current understanding, this must always print the line "here", since `emit` in the second branch starts an internal reaction and thus awakes the `await` in the first branch.

So, applying the matching transitions in order:

// Apply and-expd (p. 7)
par/@and do
    emit e;
  with
    @canrun(0);
    await e;
    _printf("here");
end

// Apply and-adv1 and emit-int, emiting the event e (p. 6/7)
par/@and do
    @canrun(0);
  with
    @canrun(0);
    await e;
    _printf("here");
end

// Apply push (p. 6)
par/@and do
    @canrun(0);
  with
    @canrun(0);
    await e;
    _printf("here");
end

Here lies the crux of the issue. The `push` transition applies `bcast` to the program description (and also increases the current stack frame and consumes the current event). `bcast` is defined as (p. 8):

bcast(p @and q, e) = bcast(p, e) @and bcast(q, e)
bcast(p; q, e) = bcast(p, e); q
bcast(@canrun(n), e) = @canrun(n)
...

Applying `bcast` to the above program yields:

// Apply @and rule
bcast(@canrun(0) @and @canrun(0); await e; _printf("here"), e) = bcast(@canrun(0), e) @and bcast(@canrun(0); await e; _printf("here"), e)

// Left @and branch
bcast(@canrun(0), e) = @canrun(0)

// Right @and branch
bcast(@canrun(0); await e; _printf("here"), e) = bcast(@canrun(0), e); await e; _printf("here")
bcast(@canrun(0); await e; _printf("here"), e) = @canrun(0); await e; _printf("here")

So, as it turns out, the @canrun primitive seems to prevent the application of the `bcast(await(e), e) = @nop` rule and thus the elimination of the `await`. Further applying the transition rules will reduce the program to:

await e;
_printf("here");

which will be forever blocked. What am I missing?

[Francisco Sant'anna]

On Fri, Dec 27, 2019, 07:55 <p.kame...@gmail.com> wrote:

Hi,

I'm trying to implement a Ceu DSL in Haskell, but I'm stuck on understanding the exact operational semantics described in the paper "A Memory-Bounded, Deterministic and Terminating Semantics for the Synchronous Programming Language Céu".

For example, let's take the following program:

par/and do
    emit e;
  with
    await e;
    _printf("here");
end

To my current understanding, this must always print the line "here", since `emit` in the second branch starts an internal reaction and thus awakes the `await` in the first branch.

...

Further applying the transition rules will reduce the program to:

await e;
_printf("here");

which will be forever blocked. What am I missing?

An emit can only awake awaits that were already awaiting before. In your example, the emit happens first. If you invert the trails, it would work as you expected. (Actually your text is different from your example.) I'm sure this is discussed and justified in one of our papers, but I'm not sure which one. I only have phone access now, but I can complete the answer in a few days.

Regards,

Francisco

[p.kame...@gmail.com]

Ah, yes - I ran through the example and it works out. The justification, as I understand is, is that in general it's easier to reason about shared state with a given predefined trail execution order.

I'm wondering, however - are you aware of any extension or modification to the transition rules that in the absence of shared state would make both programs

`emit e @and await e` and `await e @and emit e`

equivalent?

On Friday, December 27, 2019 at 5:08:42 PM UTC+2, Francisco Sant'Anna wrote:

[Francisco Sant'anna]

On Fri, Dec 27, 2019, 16:17 <p.kame...@gmail.com> wrote:

Ah, yes - I ran through the example and it works out. The justification, as I understand is, is that in general it's easier to reason about shared state with a given predefined trail execution order.

I'm wondering, however - are you aware of any extension or modification to the transition rules that in the absence of shared state would make both programs

`emit e @and await e` and `await e @and emit e`

equivalent?

Esterel uses this semantics but if a trail has a write to a variable no other trails can access that variable. Also, emits to the same event must be combined with an associate/commutative function. It also has semantics caveats known as 

"schizophrenia". Not simple at all.

In Céu, you would have to be careful with terminating par/or / breaks / emits / awaits in parallel trails, in addition to concurrent accesses.

I think it is tempting to try it in the context is Haskell. Is this a research work or something else?

Regards

[p.kame...@gmail.com]

Thanks! Will take a look at Esterel to try and figure out how they're doing things (an order-dependent @and is not very intuitive in a Haskell setting).

> I think it is tempting to try it in the context is Haskell. Is this a research work or something else?

Just a side project over the holidays :)

On Saturday, December 28, 2019 at 12:09:25 AM UTC+2, Francisco Sant'Anna wrote: