errare-humanum-est Goto Github PK

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

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

litmus-tests-riscv

RISC-V architecture concurrency model litmus tests

litmustestframework

Basic LitmusTestFramework in Cpp

murphi_grammar_extensions

openc910

OpenXuantie - OpenC910 Core

parsec-benchmark

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.

riscv-tests

rumur

yet another model checker

splash-3

The Splash-3 benchmark suite

splash-4

The Splash-4 benchmark suite

udp_joystick_emulation

A joystick emulator that turned an UDP stream coming from a MEMS into a joystick input for the flight simulator

verilator

Verilator open-source SystemVerilog simulator and lint system

vscode-murphi

Murphi language support for VS code.