Information Technology Reference
In-Depth Information
the notation
for all these forms of parallel merging, except trace parallel merge
which we denote by [][].
All these operators are associative and commutative, and the null-trace is
the identity for [][]. It is in order to get these properties that we require action
merging itself to be both associative and commutative.
Merging two microslots in parallel simply involves merging the corresponding
components:
:
MS
×
MS
→
MS
(
s
1
, q
1
, r
1
)
(
s
2
, q
2
, r
2
)
=(
s
1
♦
s
2
, q
1
♦
q
2
, r
1
♦
r
2
)
Merging microslot-sequences in parallel (
) is done on a microslot by microslot
basis, but not by merging matching pairs starting at the front of both lists, but
rather by matching the ends of the lists together with the front of the longer list
simply being copied to the result:
:
MS
∗
MS
∗
MS
∗
×
→
μ
1
μ
2
=
rev
((
rev
μ
1
)
mssaux
(
rev
μ
2
))
mssaux
μ
2
=
μ
2
μ
1
mssaux
=
μ
1
(
m
1
:
μ
1
)
mssaux
(
m
2
:
μ
2
)
=(
m
1
m
2
):(
μ
1
mssaux
μ
2
)
This counterintuitive notion of parallel merge (“merge from the back”) was dis-
covered as part of work animating these semantics[33] by encoding them in
Haskell [34]. The reason for merging in this way is to ensure that all decisions
are made as late as they possibly can be made, in particular to ensure that all
the prialts involved in generating microcycles are complete before final commu-
nication resolution is done. Intuitively, this reflects how, in the real hardware
implementations of Handel-C, we are waiting for combinatorial logic to settle
before the clock edge marking the end of the cycle, and the occurrence of the
act
-actions.
To parallel merge slots, we simply parallel-merge the microslots and action-
merge the actions:
:
Slot
×
Slot
→
Slot
(
μ
1
, a
1
)
(
μ
2
, a
2
)
=(
μ
1
μ
2
, a
1
♦
a
2
)
To merge a pair of traces we proceed on a slot-by-slot basis, and copy the longer
tail over if the traces are of different length.
[][]
:
Trc
×
Trc
→
Trc
[][]
τ
2
=
τ
2
τ
1
[][]
=
τ
1
(
s
1
:
τ
1
) [][] (
s
2
:
τ
2
)
=(
s
1
s
2
):(
τ
1
[][]
τ
2
)
Search WWH ::
Custom Search