Repository navigation
Add L2 fills and a stream prefetcher to the coherent home - #135
Closed
adambagley wants to merge 19 commits into
Closed
adambagley wants to merge 19 commits into
adambagley wants to merge 19 commits into
Conversation
…home The home had four fills and no prefetcher, so streaming code waited on one demand miss after another. Give the home L2_NUM_MSHR fills (1 to 16, eight by default, as the X3 already sets) and a prefetcher at source 3. coherence_prefetcher watches the hart requests the home accepts, from a registered copy of its D acceptance: a data table of four streams sees GetS, GetM and LoadReserved, an instruction table of two streams sees ReadOnce.IF refills. It owns four prefetch identities, presents each request from a D register, takes every source-3 G when it arrives, and loads new requests only while the home reports room for a prefetch fill. l2_stream_prefetcher gains the load enable this needs. The home looks a Prefetch up once and answers GrantAck. A resident line takes no pin, probe, read or update. An absent line gets a fill with no seat only if more than a quarter of the fills stay free, two ways of the set are available, a valid victim finds two free write-back slots, and no hart or DMA request for the block was live before the prefetch's dispatch; otherwise the prefetch completes having done nothing. A prefetch never retries, joins or waits for a fill, its engine protects no victim, it hands its sector on at its result, and it never makes a PutM wait. Demand readers take the seats of a prefetch fill and wake at its install. completion_count becomes 11*H+12: the completion table keeps four slots for the prefetch identities, so neither kind waits for the other's capacity. Those slots capture their G without G readiness, which the cluster holds set for source 3. W readiness reads one registered reduction of the fill and write-back blocks, so its depth does not grow with the fill count. Checks: the home, completion table, endpoint, cluster and stream table benches; DDR hello_world, CoreMark and ddr_bench; lint.
The completion table picked the next grant among its slots and then looked up the slot's result buffer, so the pick and its payload grew with the slot count. Rotate the grants over the eight result buffers instead: each buffer marks a ready result, the pick selects the buffer's payload directly, and the payload's tid names the slot. Rotation stays fair, now in buffer order. A prefetch changes nothing a client sees, so it no longer takes a place in the per-sector order: it neither waits for earlier requests of its sector nor holds later ones back, and the order matrix covers only the hart and DMA slots. DMA results still hand their sector on. The prefetcher takes every source-3 U when it arrives, as it takes G, and returns a table's read id only for the matching identity. Its D register loads only when empty, so its load does not wait on D readiness. The put selection no longer waits for the stop condition, which W readiness already includes, and the no-fill flag is set afresh at admission. Add the invariants the home proofs need for prefetches: a live slot holds a legal request, every tag owner is the lookup in service, the lookup's prefetch flags belong to its owner, a busy engine serves its slot's opcode, a looking-up engine has no error, and prefetches are never parked, woken or seated. The stream table proves that a request stays in the page of its stream line. Checks: the home (both line sizes), completion table and cluster benches; the completion table proofs, with and without the full address range.
The home bench takes every source-3 G when it is presented, as the prefetcher does, and its take_grant leaves those grants alone. New home cases: a Prefetch fills an absent line with no seat and leaves a resident one without a read, probe or pin; a demand read waits on a Prefetch's fill; Prefetches keep the fill reserve, the last available way and, for a valid victim, the last write-back slot; a failed Prefetch fill frees and reports the error to a joined read; Prefetches beside DMA writes and reads change no bytes; a PutM proceeds beside live Prefetches of its sector; and a demand miss replaces a line while Prefetches of every way of its set are live. The completion table bench fills both slot partitions, checks the no-fill flag against live demands of the block, and checks that a Prefetch neither waits for nor orders its sector and never holds a PutM. The cluster bench runs Prefetches through the agent port, which now carries sources 2 and 3, beside lines the L1D holds Modified. The single-hart endpoint bench recognizes the 23-slot layout. Checks: the home benches at both line sizes, the completion table, cluster (one and three L1D endpoints), endpoint and stream table benches.
The completion table proof gains a task that keeps request addresses in an eight-bit window and checks the pairwise no-fill invariant, and partition tasks with one of three slots kept for prefetches, assuming the consumer takes that slot's G when presented. The selector and arbiter proofs move from 19 to 23 inputs, the table's slot count. The home's control harness takes the fill count, the fill reserve and the tag array form as parameters. Two bounded tasks check every home assertion for 14 cycles from reset with four ways and three fills, one of them with the registered tag array; k-induction does not close with four ways. A cover task in the same configuration reaches a prefetch allocation, a prefetch that allocates nothing for a block a demand holds, prefetch fills that gain a demand seat, fail and install, and a prefetch held back by the fill reserve. coherence_prefetcher.sby proves the prefetcher's identity lifetimes, held D and C, line-aligned requests and page-bounded table requests against a home that sends one GrantAck per accepted D and a U only after C, checks the tables' read ids for 20 cycles, and covers every identity in flight, the tables taking turns and a held C. Checks: all registered tasks of coherence_home, coherence_home_completions, coherence_home_engine, coherence_home_array, coherence_home_select, coherence_control, coherence_endpoints, coherent_hart_cache and coherence_prefetcher pass.
The cache README describes how an idle grant register takes the next waiting result in rotation over the result buffers, and lists the prefetch cases of the home and cluster benches and the stream table's disabled case; the tests README lists them too. The home bench case of prefetches beside DMA writes and reads is renamed for what it checks, since prefetches no longer order other requests.
The completion table's result buffer lifetime and readiness, and each slot's result and buffer ownership flags, now take G readiness as their last term. Kept nodes hold each next state without the grant, and the presented grant's slot and buffer come from decodes of the grant registers instead of the endpoints' G valid and the slot's buffer index. An assertion ties the slot decode to the endpoints' G valid. The buffer lifetime reference check applies outside reset, since the grant registers meet the invariants the decodes rely on only after reset. The table's behavior is unchanged: the completion table bench runs the same cycles.
The work selector ranked all 23 completion slots. It now ranks twenty positions: one for each hart or DMA slot, and one after them for the four prefetch slots. That position offers a prefetch slot registered on the previous cycle, chosen in rotation among the prefetch slots and leaving out the slot being dispatched and any slot parked on that edge, so every selector input is a register. A selection needs an idle selector, which follows a dispatch by a cycle, so the offered slot is eligible whenever it can be picked; a simulation and proof assertion checks this. coherence_work_select's last input can now yield a given slot number in place of its index. A prefetch reaches an engine a cycle later than before, and at most one prefetch is picked per turn of the rotation; hart and DMA slots keep their order. The home parks no prefetch, so the prefetch position is never READY; the standalone completion-table proof now assumes this, as the composed home proof asserts. The selector proof runs the twenty-position form with a coded last input. coh_home_control_partition_prove repeats the composed home control proof with one of its three completion slots kept for prefetches.
D readiness was the OR, over the 23 completion endpoints, of each idle endpoint's admission check, which since the prefetch partition includes the endpoint's class. It now takes the same checks once from the request (legal identity and opcode, epoch, source and alignment) beside the duplicate check and the free-slot summary of the request's partition. The existing assertion that D readiness equals the chosen free endpoint's own readiness holds the two forms equal. Checks on this commit and the two before it: the completion table proofs, the selector proofs and every coherence_home task including the new partition task pass; the completion table, home (both line sizes) and cluster benches pass, with and without three L1D request endpoints, and so does DDR hello_world.
coh_completions_partition2_prove runs the completion table proof with four slots, two of them kept for prefetches, so the prefetch slots' rotation behind their shared place in the work rotation is under proof; it passes in about 190 s. Its cover task reaches the rotation passing over an offered prefetch slot. The other tasks keep three slots.
The prefetch work offer left out a prefetch slot parked on the same edge, which made the registered choice depend on the home's park decision. The home parks no prefetch, which its composed proof asserts and the standalone completion-table proof assumes, so the offer now reads only registers: the slots' eligibility and the current selection. Behavior is unchanged.
A prefetch slot holds only Prefetches, and a Prefetch never takes a fill seat, so each fill's seat selector now sees a constant zero for the prefetch slots instead of their waiting offers. The selectors rank only the hart and DMA slots, and the prefetch slots are never parked or woken by construction. Behavior is unchanged.
U readiness depends on the clients' own comparisons with the presented release. The completion table's predecessor matrix, handed flags and READY flags now take it as their last term: kept nodes hold each next state without a release on the edge (admission of a new request, DMA handoff, dispatch and wake included), and the release clears its column or slot last. READY state moves to a per-slot block for this. Behavior is unchanged. Checks on this commit and the two before it: all coherence_home_completions tasks pass; the completion table, home (both line sizes) and cluster benches, with and without three L1D request endpoints, and DDR hello_world pass with the same simulated times as before.
The held put address, which the put-blocking comparisons and the completion table's sector checks read one cycle ahead, took the incoming W's address only while W was valid. An idle put selection now offers the incoming W's address whatever W's validity: a W that is not valid leaves no put selected on the next cycle, and W readiness and the put sector checks use these comparisons only for a selected or just-accepted put. The fill and write-back owners reduce as one vector. The reference checks of the held address apply when it is the selected put's. W readiness is unchanged.
A result's match selected its slot's state, identity and address by the result's tid and compared them once. Each slot now compares the result with its own tid, state, identity and address, and the slot matches reduce through kept nodes of at most six; a DMA result's handed flag is set from its slot's match. Result acceptance is unchanged.
Each candidate of the work selector's four priority classes is now a kept node, one LUT of the slot's inputs, so the group summaries and priorities above it form a fixed tree. Selection is unchanged.
Each completion slot's result match is now two kept terms, the address comparison and the tid, state and identity comparison, which meet in one node, so the identity terms do not follow the address comparison. Result acceptance is unchanged.
Each completion slot's issue, error, wake error, count and pin flags now join READY in a per-slot block whose next states hold every other event of the edge and apply the slot's release last; a wake, a count and a pin on the release edge take effect over it, as before. Behavior is unchanged.
A release fired from the endpoints' U valid and the release arbiter's reset-gated U readiness. The completion table now forms it from the kept release candidates, which already exclude reset since an endpoint offers U only outside reset, and U readiness directly; the predecessor clear flags select their release case by U readiness alone, as reset sets them. An assertion ties the release to the arbiter's handshake. Behavior is unchanged. Checks on this commit and the five before it: all coherence_home_completions and coherence_home tasks pass; the completion table, home (both line sizes) and cluster benches, with and without three L1D request endpoints, and DDR hello_world pass with the same simulated times.
The overview gives the home's eight fills and its prefetching of data and instruction streams. The roadmap no longer lists four fills and a missing stream prefetcher among the costs of the coherent path, and its memory system paragraph gives the home's fill count and the prefetcher's requests in place of the plan to add them.
Collaborator
Author
|
Superseded by #147. |
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
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.
The coherent home gets L2_NUM_MSHR fills, eight by default, with a quarter kept for demand misses. It also gets a stream prefetcher at its own source, which follows the harts' data streams and instruction refill streams and reads ahead of L1 misses into the L2. A prefetch allocates a fill only when the line is absent, enough fills are free and no demand wants the block. It never waits, joins a fill or holds a line. README.md and ROADMAP.md describe the home's fills and prefetcher.
DDR CoreMark runs 2.5% faster, and CoreMark-PRO's DDR workloads run 0.2 to 10.9% faster (zip 10.9%, sha 6.8%, parser 4.3%). ddr_bench's streaming kernels take 17 to 22% fewer cycles. BRAM CoreMark is unchanged. The only slowdowns above 0.2% are in a self-modifying-code stress test, smc_fencei_test in DDR: +1.8%, and +1.3% with equal line sizes.
The completion table, home, prefetcher and selector proofs pass, as do the home, cluster and endpoint benches, the program set in both memory configurations, seeded runs, lint, the fast tests and synthesis.