Translating initialise concepts to STGs

[snowleopard]

@jrbeaumont and I are looking into the following problem.

We have two handshake concepts left and right with initial states:

left  = handshake00 a b
right = handshake00 c d

We also have a third handshake concept mid without an initial state:

mid = handshake b c

We want to be able to compose all three concepts and translate them into an STG in such a way that the mid handshake picks up the correct initial state. That is, the following system concept

system = left <> mid <> right

should be equivalent to the concept with explicit initialisation:

system' = left <> handshake00 b c <> right

We have been trying to play with possible STGs corresponding to the mid concept but so far no complete solutions. This is the thread to discuss possible solutions.

[mvdan]

So it would be up to the translator to figure out the missing initializations? Would this require simulating the circuit?

[snowleopard]

@mvdan One specific question: which STG should be produced for the mid concept?

One requirement: when composed with STGs for left and right using parallel composition (e.g. in Workcraft), the result should be equivalent to translating system' to an STG.

Regarding simulation: the mid concept should allow any transition to occur initially, but then follow the standard handshake pattern. Basically we should be able to get one of the following 4 behaviours:

• b+ -> c+ -> b- -> c- -> ...
• c+ -> b- -> c- -> b+ -> ...
• b- -> c- -> b+ -> c+ -> ...
• c- -> b+ -> c+ -> b- -> ...

Does this hold already? I don't know, we need to check :)

[snowleopard]

Let me also clarify the rationale.

We want to allow undefined or not completely defined initial states to allow for more reuse of concepts and for their better compositionality. One can imagine a hardware component that is fine to be in one of two possible initial states. When connected to a different component which only supports one initial state we should get a working system with only one initial state -- the one which is allowed by both components.

It may well be that what we want is not possible and we need to always be explicit about initial states. But I hope this is not the case.

[mvdan]

Sounds to me like this could be solved by simply brute forcing all the combinations of possible initial states which are undefined. Granted that such bruteforce method might not scale well at all, but if it can be proven to work then this can definitely be done. Then we can look at ways to be smarter around it.

[mvdan]

Which also makes me think that we might encounter that there are no possible valid combinations for a composed circuit.

[snowleopard]

@mvdan Note: the set of compatible initial states is not difficult to obtain. It is exactly the Boolean AND of all initial predicates. In our case, it is:

initialStates = initial left .&&. initial mid .&&. initial right

or equivalently:

initialStates = initial $ left <> mid <> right

[mvdan]

I'm confused then. Why isn't this the answer we're looking for?

[jrbeaumont]

We are aiming to try and find a more general solution. I'm going to do some tests, see what we can find, and what we can see to avoid. For example, in mid above, we wan't to avoid: b- -> c+ -> c-

[snowleopard]

@mvdan Let me repeat the question: which STG should be produced for the mid concept alone? :)

[mvdan]

Assuming you mean the undefined initial states, for a handshake alone I'd guess we want either 00 or 11 to avoid an extra enabled transition.

[snowleopard]

The STG for mid should contain the following behaviours:

• b+ -> c+ -> b- -> c- -> ...
• c+ -> b- -> c- -> b+ -> ...
• b- -> c- -> b+ -> c+ -> ...
• c- -> b+ -> c+ -> b- -> ...

But not the ones like @jrbeaumont mentioned:

• b+ -> b- -> ...
• c+ -> c- -> ...

Such an STG would compose nicely with STGs that do have well-defined initial states.

And it should also be relatively understandable, as otherwise it would be difficult to derive automatically.

[snowleopard]

Let me upload some STGs here: example.zip.

The archive contains left.work, mid.work and right.work with handshake STGs as described above.

The mid.work is probably want we want according to the previous comment. It does allow 4 correct behaviours. I obtained it by contracting dummies in the solution with 4 dummies.

However, composing these three STGs still leads to a deadlock after parallel composition. Which is unexpected to me. Any thoughts? Can we eliminate the deadlock in any way?

[jrbeaumont]

An example which offers initialisation for just the input b in mid works correctly. Whichever state b is initialised to implies the initial state of c. This is shown in: Example2.zip

I may test this theory with the replacement of mid with a C-element. Both it's inputs are set by a separate handshake for example left1 and left2. The output connects to right

Edit: A C-element proves an issue: in the event that the inputs are initially 1 0 or 0 1 then the output could be either 0 or 1 initially

[snowleopard]

Thanks @jrbeaumont! I am starting to think that we can't compose arbitrary left and right handshakes with mid: they need to be aligned somehow as otherwise we should and will get into a deadlock.

[jrbeaumont]

I agree, and a CElement provides a whole new set of problems. I will have a think about what we can use instead of left and right. However, I feel as a simple test mid will be useful to keep. What do you think?

[snowleopard]

@jrbeaumont Coming back to the case with three handshakes. Could you do the following experiment?

• Let left be simply handshake00 a b.
• Let mid be handshake b c as before.
• Try all four possible handshakes for right and let us know which will lead to deadlocks after composing all handshakes together. We can try to spot a pattern there.

For mid use the STG from example.zip.

[jrbeaumont]

If right is: handshake00 c d then there is a deadlock. handshake c d <> initialise c 1 <> initialise d 0 (handshake10 c d) there is a deadlock handshake11 c d then there is a deadlock handshake c d <> initialise c 0 <> initialise d 1 (handshake01 c d) there is a deadlock

This seems to not help :(

[jrbeaumont]

OK, I have tested mid with the automatic initialisations for just the input (b) and then the output (c) and then composed this with all possible combinations for right. The results are as follows: Inputs only when right is: handshake00 - No deadlocks. handshake10 - Deadlocks. handshake11 - Deadlocks. handshake01 - No deadlocks.

Outputs only when right is: handshake00 - Deadlocks. handshake10 - No deadlocks. handshake11 - No deadlocks. handshake01 - Deadlocks.

This maybe doesn't answer any questions, but the meeting gave us more ideas, and somewhat more useful than this test. However I wanted to try this anyway just to see what the outcome was.

The files are attached. example3.zip

[snowleopard]

@jrbeaumont Thanks, looks curious! Something XOR-ry is clearly going on :)

By the way, I think the following concept forces the initial state of mid to be either 00 or 11.

mid = handshake b c <> initialiseEqual b c

initialiseEqual a b = initialiseConcept $ \State value -> value a == value b

[jrbeaumont]

I know what you mean, hard to explain why it works, but at least it doesn't deadlock in every case as it was before.

This concept would work, assuming that anything it is composed with contains an initial state for one of these signals.

[jrbeaumont]

Added in PR #39.