Synchronized Operator

Syntax

processBehaviour “||” processBehaviour

Semantics

process1 || process2

process1 and process2 are executed while synchronized over all channels, including EXIT.

When both processes have exited then the synchronized composition exits.

Examples

Communication

The statement

    Channel1_Int ? x
||
    Channel1_Int ? y
describes the process with two sub processes that are synchronized over all channels.
Since both sub processes want to communicate over Channel1_Int, communication is possible.
After that communication has occurred x and y contain the same value, and
since both communications have exited, the synchronized composition exits.

Constrained communication

The statement

    Channel1_Int ? x [[ x >= 10 ]]
||
    Channel1_Int ? y [[ y <= 20 ]]
describes the process with two sub processes that are synchronized over all channels.
Since both sub processes want to communicate over Channel1_Int and
both constraints can be simultaneously satisfied, communication is possible.
After that communication has occurred x and y contain the same value in the range [10,20]
and, since both communications have exited, the synchronized composition exits.

Deadlock

The statement

    Channel1_Int ? x
||
    Channel2_Int ? y
describes the process with two sub processes that are synchronized over all channels.
Since one sub process wants to communicate the variable x over Channel1_Int and
the other sub process wants to communicate the variable y over another channel, Channel2_Int,
communication under the synchronization constraint is not possible, i.e., the process is in deadlock.