Pinned Repositories
antlr3
antlr v3 repository (pulled from p4 with history from //depot/code/antlr/antlr3-main
CMurphi
Download_Manager_Tool
A tool developed as part of the TUM Multimedia Communication course to download a file from a server using a dash_daemon application provided by the course instructor
Dve_Protocol_Model_Check
ProtoGen pcc protocol implementations of Dvé: Coherent Replication Protocol
gem5-Trace-Checker
A python script that can be used to parse gem5 traces to search for deadlocks. Will be extended to support additional statistics in the future.
HeteroGen
We solve the two challenges architects face when designing heterogeneous processors with cache coherent shared memory. First, we develop an automated tool, called HeteroGen, for composing clusters of cores, each with its own coherence protocol. Second, we show that the output of HeteroGen adheres to a precisely defined memory consistency model that we call a compound consistency model. For a wide variety of protocols --- including the MOESI variants, as well as those that are targeted towards Total Store Order and Release Consistency --- we show that HeteroGen can correctly fuse them. To validate HeteroGen, we develop the first litmus tests for verifying that heterogeneous protocols satisfy compound consistency models. To understand the possible performance implications of automatic protocol generation, we compared against a publicly available manually-generated heterogeneous protocol. Our results show that performance is comparable.
HieraGen
We present HieraGen, a new tool for automatically generating hierarchical cache coherence protocols. HieraGen's inputs are the simple, atomic, stable state protocols for each level of the hierarchy. HieraGen's output is a highly concurrent hierarchical protocol, in the form of the finite state machines for all of the cache and directory controllers. HieraGen thus reduces the complexity that architects face, by offloading the challenging tasks of composing protocols and managing concurrency. Experiments show that HieraGen can automatically generate correct-by-construction MOESI family of hierarchical protocols with dozens of states and hundreds of transitions. We have verified all of the generated protocols for safety and deadlock freedom using a model checker.
Linearization-Protocol
Verification of the Linearization Protocol proposed in: Scale-out CcNUMA: Exploiting Skew with Strongly Consistent Caching
PhD-Thesis
PhD Thesis
ProtoGen
Designing directory cache coherence protocols is complicated because coherence transactions are not atomic in modern multicore processors. A coherence transaction comprises multiple messages, and these messages can interleave with other conflicting coherence transactions initiated by other cores. To overcome this architectural challenge, we present ProtoGen, an automated tool for taking the description of a directory protocol with atomic transactions (i.e., no concurrency) and generating the corresponding protocol for a multicore with non-atomic transactions. ProtoGen outputs the finite state machines for the cache and directory controllers, including all of the transient states that are possible with concurrent transactions. We have used ProtoGen to generate complete MSI, MESI, and MOSI protocols given their stable state protocol specifications. We have verified the generated protocols for safety and deadlock freedom using the Murϕ model checker. Our generated protocols are identical to or better than manually generated protocols, at times even discovering opportunities to reduce stalling.
Errare-humanum-est's Repositories
Errare-humanum-est/ProtoGen
Designing directory cache coherence protocols is complicated because coherence transactions are not atomic in modern multicore processors. A coherence transaction comprises multiple messages, and these messages can interleave with other conflicting coherence transactions initiated by other cores. To overcome this architectural challenge, we present ProtoGen, an automated tool for taking the description of a directory protocol with atomic transactions (i.e., no concurrency) and generating the corresponding protocol for a multicore with non-atomic transactions. ProtoGen outputs the finite state machines for the cache and directory controllers, including all of the transient states that are possible with concurrent transactions. We have used ProtoGen to generate complete MSI, MESI, and MOSI protocols given their stable state protocol specifications. We have verified the generated protocols for safety and deadlock freedom using the Murϕ model checker. Our generated protocols are identical to or better than manually generated protocols, at times even discovering opportunities to reduce stalling.
Errare-humanum-est/HeteroGen
We solve the two challenges architects face when designing heterogeneous processors with cache coherent shared memory. First, we develop an automated tool, called HeteroGen, for composing clusters of cores, each with its own coherence protocol. Second, we show that the output of HeteroGen adheres to a precisely defined memory consistency model that we call a compound consistency model. For a wide variety of protocols --- including the MOESI variants, as well as those that are targeted towards Total Store Order and Release Consistency --- we show that HeteroGen can correctly fuse them. To validate HeteroGen, we develop the first litmus tests for verifying that heterogeneous protocols satisfy compound consistency models. To understand the possible performance implications of automatic protocol generation, we compared against a publicly available manually-generated heterogeneous protocol. Our results show that performance is comparable.
Errare-humanum-est/HieraGen
We present HieraGen, a new tool for automatically generating hierarchical cache coherence protocols. HieraGen's inputs are the simple, atomic, stable state protocols for each level of the hierarchy. HieraGen's output is a highly concurrent hierarchical protocol, in the form of the finite state machines for all of the cache and directory controllers. HieraGen thus reduces the complexity that architects face, by offloading the challenging tasks of composing protocols and managing concurrency. Experiments show that HieraGen can automatically generate correct-by-construction MOESI family of hierarchical protocols with dozens of states and hundreds of transitions. We have verified all of the generated protocols for safety and deadlock freedom using a model checker.
Errare-humanum-est/CMurphi
Errare-humanum-est/antlr3
antlr v3 repository (pulled from p4 with history from //depot/code/antlr/antlr3-main
Errare-humanum-est/Download_Manager_Tool
A tool developed as part of the TUM Multimedia Communication course to download a file from a server using a dash_daemon application provided by the course instructor
Errare-humanum-est/Dve_Protocol_Model_Check
ProtoGen pcc protocol implementations of Dvé: Coherent Replication Protocol
Errare-humanum-est/gem5-Trace-Checker
A python script that can be used to parse gem5 traces to search for deadlocks. Will be extended to support additional statistics in the future.
Errare-humanum-est/Linearization-Protocol
Verification of the Linearization Protocol proposed in: Scale-out CcNUMA: Exploiting Skew with Strongly Consistent Caching
Errare-humanum-est/Link_Rate_Measurement_Tool
A tool developed as part of the TUM Multimedia Communication course to measure the link rate of a data streaming service
Errare-humanum-est/PhD-Thesis
PhD Thesis
Errare-humanum-est/litmus-tests-riscv
RISC-V architecture concurrency model litmus tests
Errare-humanum-est/LitmusTestFramework
Basic LitmusTestFramework in Cpp
Errare-humanum-est/Murphi_Grammar_Extensions
Errare-humanum-est/openc910
OpenXuantie - OpenC910 Core
Errare-humanum-est/parsec-benchmark
Errare-humanum-est/riscv-tests
Errare-humanum-est/rumur
yet another model checker
Errare-humanum-est/Splash-3
The Splash-3 benchmark suite
Errare-humanum-est/Splash-4
The Splash-4 benchmark suite
Errare-humanum-est/UDP_Joystick_Emulation
A joystick emulator that turned an UDP stream coming from a MEMS into a joystick input for the flight simulator
Errare-humanum-est/verilator
Verilator open-source SystemVerilog simulator and lint system
Errare-humanum-est/vscode-murphi
Murphi language support for VS code.