Causality Analysis: False positive?

[Matthias]

Hi Blech Team,

I have implemented the following Blech code:

@[EntryPoint]
activity Main ()()
  var i: nat8 = 42
  cobegin
    await true
    i = 5 // A
  with
    i = i + 1 // B
  end
end

This code is rejected by blechc due to a write-write causality error. In the boot reaction i will be set to 42 and then re-set to 43 (i = 42 + 1) immediately when entering the cobegin block. Then the reaction ends. In the next reaction i will be set to 5. So from my understanding write access A and B can never happen in the same reaction – means no concurrent write access and hence no violation of causality.

Why is this code rejected by the Blech compiler? Is it a limitation of the causality analysis or maybe a deliberate design decision?

Thanks in advance!

Best regards,

Matthias

[Gretz Friedrich (CR/AEE1)]

Hallo Matthias,

indeed this program must be rejected and this is a deliberate choice. We take a “thread local” view (cf. https://github.com/boschresearch/blech-doc/blob/master/documentation/blech-user-manual/controlflow.adoc#causality) which means there are two threads that both want to write variable i. The exact reaction is irrelevant. Of course, this is an over-approximation in this particular case. But in general these write operations may come after await statements with different conditions and the compiler cannot guarantee that they exclude one another.

 

Note that your example is a sequential program in nature. It would be interesting to see if you can find a practical example in which

-          concurrency is needed

-          writing from at least two threads to a shared variable is needed

-          you can statically determine that these writes do not interfere

Given such an example, we could discuss if we can find patterns how to rewrite it in Blech.

 

Cheers,

Friedrich

--
You received this message because you are subscribed to the Google Groups "blech-lang" group.
To unsubscribe from this group and stop receiving emails from it, send an email to blech-lang+...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/blech-lang/f7c6c5df-2287-4996-948f-26e22da14b64%40googlegroups.com.

[Matthias]

Hi Friedrich,

thanks for the detailed explanation. Actually, I just used this example for getting a better understanding of how exhaustive the causality analysis is working. I was just wondering whether it explicitly checks all the possible combinations of any two write accesses between any two concurrent trails. So as far as I understood from your explanation the code will be rejected as soon as two concurrent trails potentially could write-access a shared variable in the same reaction – irrespective of whether this situation will actually occur or not.

Best regards,

Matthias

To unsubscribe from this group and stop receiving emails from it, send an email to blech-lang+unsubscribe@googlegroups.com.

[Gretz Friedrich (CR/AEE1)]

That’s right J

 

Best,

To unsubscribe from this group and stop receiving emails from it, send an email to blech-lang+...@googlegroups.com.

To view this discussion on the web, visit https://groups.google.com/d/msgid/blech-lang/f7c6c5df-2287-4996-948f-26e22da14b64%40googlegroups.com.

--

You received this message because you are subscribed to the Google Groups "blech-lang" group.

To unsubscribe from this group and stop receiving emails from it, send an email to blech-lang+...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/blech-lang/928dfa5f-3fb3-4b00-a613-a5e13c5e3f64%40googlegroups.com.