Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

CQueue: rework implementation #11

Open
NicolasT opened this issue Mar 21, 2023 · 2 comments
Open

CQueue: rework implementation #11

NicolasT opened this issue Mar 21, 2023 · 2 comments
Assignees
Labels
enhancement New feature or request

Comments

@NicolasT
Copy link
Owner

The current implementation of CQueue is quite complicated. Reworking this, simplifying it, potentially making it fully STM-only, could be useful.

See: #7

@NicolasT NicolasT added the enhancement New feature or request label Mar 21, 2023
@NicolasT
Copy link
Owner Author

Note, making this STM-only, is potentially not a good idea, though we likely do want to make "most of it" run in STM, but potentially multiple transactions.

The rationale: a receive should not impact any send, to the max extent possible. If we run the whole receive inside a single transaction, then either it will succeed but any sends will need to be restarted, or a receive transaction would be interrupted by any send and need to retry. All this could lead to some livelock'y situations.

The way this could be implemented (though to be validated/discussed/...) is by running a first transaction in receive which empties the message queue and puts all messages in some other TVar value (akin to what the current CQueue implementation does). Since there are no guarantees about handling of messages which arrive during a call to receive, from that point on, sends can put messages in the TQueue again without being impacted by, or impacting, the receive. In a subsequent transaction, messages stored in this TVar can be consumed by receive (as well as any other STM values): no send will be impacted, nor will any send impact this second transaction.

@NicolasT
Copy link
Owner Author

It's likely a good idea to model the implementation using DejaFu or IOSim and have tests in place to validate the properties we expect the implementation to adhere to. See also #17.

NicolasT added a commit that referenced this issue Mar 27, 2023
This patch simplifies the `receive*` machinery, introducing an `after`
`Match` which uses STM's `registerDelay` to implement a `receive` with
timeouts, instead of relying on `CQueue`s `Timeout` and `NonBlocking`
implementations.

This should ease reworking `CQueue`, since there should be no need for
a distinction between blocking, timeout and non-blocking behaviour in
its implementation. Hence, from now on, `troupe` only uses `CQueue`s
`Blocking` `dequeue` method.

See: #12
See: #11
NicolasT added a commit that referenced this issue Mar 27, 2023
This patch simplifies the `receive*` machinery, introducing an `after`
`Match` which uses STM's `registerDelay` to implement a `receive` with
timeouts, instead of relying on `CQueue`s `Timeout` and `NonBlocking`
implementations.

This should ease reworking `CQueue`, since there should be no need for
a distinction between blocking, timeout and non-blocking behaviour in
its implementation. Hence, from now on, `troupe` only uses `CQueue`s
`Blocking` `dequeue` method.

See: #12
See: #11
NicolasT added a commit that referenced this issue Mar 27, 2023
This patch simplifies the `receive*` machinery, introducing an `after`
`Match` which uses STM's `registerDelay` to implement a `receive` with
timeouts, instead of relying on `CQueue`s `Timeout` and `NonBlocking`
implementations.

This should ease reworking `CQueue`, since there should be no need for
a distinction between blocking, timeout and non-blocking behaviour in
its implementation. Hence, from now on, `troupe` only uses `CQueue`s
`Blocking` `dequeue` method.

See: #12
See: #11
@NicolasT NicolasT self-assigned this Mar 27, 2023
NicolasT added a commit that referenced this issue Mar 27, 2023
NicolasT added a commit that referenced this issue Mar 29, 2023
This patch simplifies the `receive*` machinery, introducing an `after`
`Match` which uses STM's `registerDelay` to implement a `receive` with
timeouts, instead of relying on `CQueue`s `Timeout` and `NonBlocking`
implementations.

This should ease reworking `CQueue`, since there should be no need for
a distinction between blocking, timeout and non-blocking behaviour in
its implementation. Hence, from now on, `troupe` only uses `CQueue`s
`Blocking` `dequeue` method.

See: #12
See: #11
NicolasT added a commit that referenced this issue Mar 29, 2023
This patch simplifies the `receive*` machinery, introducing an `after`
`Match` which uses STM's `registerDelay` to implement a `receive` with
timeouts, instead of relying on `CQueue`s `Timeout` and `NonBlocking`
implementations.

This should ease reworking `CQueue`, since there should be no need for
a distinction between blocking, timeout and non-blocking behaviour in
its implementation. Hence, from now on, `troupe` only uses `CQueue`s
`Blocking` `dequeue` method.

See: #12
See: #11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
enhancement New feature or request
Projects
None yet
Development

No branches or pull requests

1 participant