Add ReqResp Protocol

[lmbollen]

A simple protocol for request-response communication. The forward channel channel has type Signal dom (Maybe req) and is used to send requests, the backward channel has type Signal dom (Maybe resp) and is used to send responses.

The protocol must obey the following rules:

• When the forward channel is Just a, it must not change until the transaction is completed.
• The forward channel can not depend on the backward channel.
• When the forward channel is Nothing, the backward channel may be undefined.
  Currently only the basic protocol definition is there, I'm looking for feedback and extra desired functionality.

[martijnbastiaan]

In general I don't see an issue with this protocol, but I'm do wondering if there is a way where we can formalize a little bit what kind of protocols there are / can be. Right now we're kinda slapping on protocol after protocol.

[martijnbastiaan]

Suggested change

	-- * When the forward channel is @Nothing@, the backward channel may be undefined.
	-- * When the forward channel is @Nothing@, the backward channel may not be observed.

In the previous wording you could try to transfer data over the backward channel when the forward channel would be Nothing, but given the name of the protocol I think this is not the intention.

[DigitalBrains1]

So is this:

• If the forward channel is Nothing, it can happen that the backward chanel is not observed
• If the forward channel is Nothing, you are not allowed to look at the backward channel

I'd say the latter, and your phrasing is still ambiguous. I vote either "shall not" or "must not".

[martijnbastiaan]

Suggested change

	-- \| Forward channel for ReqResp protocol:
	-- | Forward channel for ReqResp protocol:

What happened here?

[martijnbastiaan]

Suggested change

	-- and the backward channel is used to send responses.
	-- Rules:
	-- and the backward channel is used to send responses.
	--
	-- Rules:

new paragraph = newline

[martijnbastiaan]

Can you write this as a paragraph instead of loose sentences?

[Losiek]

This implies that this protocol can not be pipelined. We can relax this constraint and do two versions of ReqResp (pipelined and not pipelined). Or we can use DSignal to enforce different pipeline depths on the type level.

[rowanG077]

Why couldn't it be pipelined? I think you can write a component that handles this. Essentially store forward in a register. Send contents of the register to the sink. When the sink responds either send it directly to the source and clear the register or put the response in a register as well. The main problem is that you no longer can have full throughput between source and sink.

[christiaanb]

Perhaps we should then just have

type ReqRespPipelined (dom :: C.Domain) (req :: Type) (resp :: Type) = (Df dom req, Reverse (Df dom resp))

a kind of Axi4LiteLite

[DigitalBrains1]

Enforcing pipeline depth on the type level seems to be more useful than just a blanket declaration "you can send stuff, which we call a request, and you can receive stuff, which we call a response", which seems to be what Christiaans ReqRespPipelined is.

Avalon Stream does pre-negotiated pipelining. You can configure that when you drop ready, you can still receive data in the next n cycles, so the pipeline of the sender can empty. Constructions like that. Maybe it can serve as inspiration.

Alternatively, we can tackle pipelining in a different PR.

[lmbollen]

I don't think separating the channels is a good idea as it directly contradicts the purpose of circuit-notation (Combining forward and backward channels in a single binder).

How about separating request acknowledgement and response timing?:

data ReqResp (dom :: C.Domain) (req :: Type) (resp :: Type)

instance Protocol (ReqResp dom req resp) where
  -- | Forward channel for ReqResp protocol
  type Fwd (ReqResp dom req resp) = C.Signal dom (Maybe req)

  -- | Backward channel for ReqResp protocol
  type Bwd (ReqResp dom req resp) = C.Signal dom (Bool, Maybe resp)

Here the Bool would indicate a request acknowledgement and Maybe resp could be Just resp later.
Combinatorial circuits could then return (isJust resp, resp).

[DigitalBrains1]

How would you still be able to tell which response corresponds to which request?

Never mind, that's not a very clever comment.

It does seem to me that you need a whole bunch more protocol specification for two pipelined implementations to be able to communicate. Where's the guarantees? I want to know I can still get rid of all the data currently in my pipeline; if I can't get a guarantee I can deliver it all, I will need buffers to deal with the case that I cannot, or I need to be able to stall the whole pipeline at any random moment, and we're back at square one.

Personally, I think a "simple" protocol that doesn't allow pipelining at the protocol level¹ and a separate more complex protocol that tackles pipelining in a neat and efficient way is a perfectly fine solution. This PR can be the simple variant.

¹ As Rowan indicates above, you can still accomodate pipelining with constructions like skid buffers, but the protocol would be oblivious to this and it would in general be less efficient than pipelining being part of the protocol.

[t-wallet]

Looks good. This is the generic version of the ArpLookup protocol (to be upstreamed to clash-cores), so we can nicely specify that in terms of ReqResp. We did not need more functionality than just the protocol definition there, so I don't have anything to add for now.

[bgamari]

It turns out that I have done something very similar to this in #109.

[lmbollen]

It turns out that I have done something very similar to this in #109.

Great minds think alike it seems ;)

Your pull request already has tests so I'm inclined to continue with that one.
One thing I'm missing is the distinction between BiDf masters and BiDf slaves.
Shall I close this PR in favor of yours?

[DigitalBrains1]

[edit] Woops I apparently didn't read the documentation.

That just leaves one comment: please, no masters and slaves. Please use manager and subordinate or something else like that.
[/edit]

[edit 2]
I think it looks pretty clear:

type BiDf dom req resp =
  (Df dom req, Reverse (Df dom resp))

That means requests go forward and responses go backward, right? The documentation uses downstream and upstream, maybe it were more clear if that would be in the forward(backward) direction, but the names of the tyvars in BiDf are also a form of documentation.
[/edit 2]