Split bounded-queue credits and add model-based tests - #3
Open
SamuelSchlesinger wants to merge 1 commit into
Open
Split bounded-queue credits and add model-based tests#3SamuelSchlesinger wants to merge 1 commit into
SamuelSchlesinger wants to merge 1 commit into
Conversation
Bounded queues tracked occupancy in a single TVar that every enqueue and every dequeue wrote, so producers and the consumer conflicted on every operation even though the queue's two-TVar layout keeps their fast paths apart. Track free capacity as split read and write credits instead, in the style of TBQueue: enqueue spends write credits, dequeue and flush release read credits, and only an enqueue that finds no write credits moves the read credits over. Capacity accounting now conflicts once per `limit` enqueues rather than once per operation. Move the implementation to Data.Queue.Internal so tests can check the representation invariants, with Data.Queue re-exporting the public API. Add a QuickCheck model test that runs random operation sequences against a FIFO list and checks the invariants after every step, a multi-producer stress test, and a bounded Queue versus TBQueue throughput benchmark.
4 tasks
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
TVarthat everyenqueueand everydequeuewrote, so producers and the consumer conflicted on every operation — undoing the two-TVarlayout's separation of the fast paths. This tracks free capacity as split read/write credits in the style ofTBQueue:enqueuespends write credits,dequeue/flushrelease read credits, and only anenqueuethat finds no write credits moves the read credits over. Conflicts on capacity accounting drop from once per operation to once perlimitenqueues.Data.Queue.Internal(documented as outside the PVP) so tests can check the representation invariants;Data.Queuere-exports the same public API.length bs <= length ts, front empty iff queue empty, credits == free capacity), a multi-producer stress test, and a--throughput-boundedbenchmark comparing boundedQueuewithTBQueue.rotateto WHNF like the dequeue side already did.Measurements (GHC 9.6.7,
-N8, 1 s wall clock, P senders -> 1 consumer)Ranges span several runs; absolute numbers move a lot between runs on this machine but the ordering within a run is stable. Single-thread cost rises ~10% from the extra branch.
Test plan
cabal build --enable-tests --enable-benchmarks --ghc-options=-Werror allcabal test— 22 examples incl. 1,000 model-test cases and the fan-in stress test (unbounded, capacity 16, capacity 1)cabal check,cabal haddock --haddock-for-hackage,cabal sdiststm-queue-benchmark --throughput-bounded