Skip to content

Add Lookahead, the dual to Pipelined#93

Open
nfrisby wants to merge 2 commits into
mainfrom
nfrisby/lookahead
Open

Add Lookahead, the dual to Pipelined#93
nfrisby wants to merge 2 commits into
mainfrom
nfrisby/lookahead

Conversation

@nfrisby

@nfrisby nfrisby commented Jul 24, 2026

Copy link
Copy Markdown
Contributor

This PR supersedes PR #92. Same key idea: be able to receive (pipelined) messages possibly before sending response when you have the agency. But with better names, types, UX, etc.

The key semantic change was explained here: #92 (comment)

I've converted back to Draft because I think I realized why YieldPipelined is the way it is (ie why it "unnecessarily" couples "one Receiver with one send"): so that the Pipelining n is counting the number of pipelined messages. Because a principal concept when pipelining is the depth, so it's nice and helpful and expected for the current depth to equal n (or, well, n can be greater than the current depth but only if you haven't tried Collecting).

I'm now thinking through whether we want that same thing to be true on the DualPipelined n server: should it count (subject to DualCollect calls), the number of pipelined messages that the server has read? IE the number of received messages the server still owes a response to (where "response" might involve sending 1 or more messages).

#92 (comment)

nfrisby added 2 commits July 24, 2026 08:00
This is intended to run on servers, which means there will be potentially
hundreds of instances. Therefore, it can be worthwhile for a driver to use
merely a counter rather than a queue; hence the motivation for FixedSender and
TheSender.
@nfrisby
nfrisby requested a review from a team as a code owner July 24, 2026 12:08
@nfrisby

nfrisby commented Jul 24, 2026

Copy link
Copy Markdown
Contributor Author

With the new interface, the motivating use case (originally listed here #92 (comment)) now looks as follows:

  leiosNotifyServerPeerLookahead ::
    forall m point announcement vote.
    MonadThrow m =>
    m Bool ->
    -- ^ increments the number of outstanding requests
    m (Message (LeiosNotify point announcement vote) StBusy StIdle) ->
    -- ^ blocks until the next reply (announcement\/offer\/vote) is ready
    PeerLookaheadFixedSender (LeiosNotify point announcement vote) AsServer StIdle m ()
  leiosNotifyServerPeerLookahead incr next =
      PeerLookaheadFixedSender responder start
    where
      responder :: Sender (LeiosNotify point announcement vote) AsServer VariableSender StBusy StIdle m
      responder = SenderEffect $ next <&> \msg -> SenderYield ReflServerAgency msg SenderDone

      -- StIdle with nothing outstanding: receive the first request (or done).
      -- We must use a plain Await here: AwaitLookahead defers the StBusy->StIdle
      -- send, so it is only usable once we hold a request (i.e. are at StBusy).
      start ::
        Peer (LeiosNotify point announcement vote) AsServer (Lookahead Z (FixedSender StBusy StIdle)) StIdle m ()
      start =
        Await ReflClientAgency $ \case
          MsgDone                         -> Done ReflNobodyAgency ()
          MsgLeiosNotificationRequestNext ->
            Effect $ do
              incr >>= \b -> when b $ throwIO MkExnLeiosNotifyExcessiveRequests
              pure $ busy Zero

      -- StBusy with @n@ outstanding: hand this reply off to the responder and
      -- look ahead to the next request (or done), in one step.
      busy :: forall n.
        Nat n ->
        Peer (LeiosNotify point announcement vote) AsServer (Lookahead n (FixedSender StBusy StIdle)) StBusy m ()
      busy n =
        AwaitLookahead TheSender ReflClientAgency $ \case
          MsgDone                         -> drain (Succ n)
          MsgLeiosNotificationRequestNext ->
            Effect $ do
              incr >>= \b -> when b $ throwIO MkExnLeiosNotifyExcessiveRequests
              pure $ busy (Succ n)

      -- on termination, flush the sends we've handed off, then Done.
      drain :: forall n.
        Nat n ->
        Peer (LeiosNotify point announcement vote) AsServer (Lookahead n (FixedSender StBusy StIdle)) StDone m ()
      drain = \case
        Zero   -> Done ReflNobodyAgency ()
        Succ j -> FlushSender Nothing (drain j)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant