Projects

This is a list of project ideas to get you started on thinking about your project. Note that these are not complete detailed project specifications: you would need to discuss with your team and myself to come up with a clear specification. You are of course welcome to come up with your own project - please discuss with me. 

1. Specifying coherence protocols formally. There are number of public coherence protocol specifications which are in prose. The goal of the project is to first specify them in a table format as in the Primer (Chapter 8), and then formally model them in a model checker. Here is a sample project Download sample project that does this for the CHI Links to an external site. protocol specification. You can formalize specifications such as CXL Download CXL, TileLink Links to an external site., or Open-CAPI. 

2. Deducing the consistency model of systems using litmus testing. The goal of the project is to consider any distributed memory system -- e.g., (a) CPU and GPUs connected via PCIe (b) CPU and NIC connected by PCIe (c) any key-value-store or a data base -- and deduce its consistency model behavior. Please refer to the papers on consistency specification on how to do this (e.g., paper1 Links to an external site., paper2 Links to an external site.)

3. Is sequential consistency (SC) actually easier to program compared to relaxed Consistency? 

Sequential Consistency, the strongest consistency model is thought be the most programmable of memory consistency models, and this fact is repeated again and again in many research papers and articles. But is this really true? Nobody knows for sure. In this project, you will investigate whether this is true by conducting a well-designed user study.  You will carefully arrive a small programming problem specification, and carefully consider a relaxed memory model, depending on your hypothesis you want to establish. Then you want to analyze the results and draw insights. 

4.  Specifying Heterogeneous Consistency. Recent work has come up with Compound Consistency Models Links to an external site. - a compositional amalgamation of memory models. That approach used an operational approach to composing memory models. Today, however, companies used the axiomatic method to expressing memory models using tools such as Herd Links to an external site. or Alloy Links to an external site.. The goal of the project is to express compound memory models axiomatically in a tool such as Herd. Another possibility is to extend our work Links to an external site. and express other compound memory models such as the ARM/x86 model, ARM/PTX model etc. 

5. Hermes Links to an external site., Kite Links to an external site. (and other protocols expressed in Odyssey Links to an external site.) are examples of replication protocols for emulating fault-tolerant shared memory. The goal of the project is to employ this fault-tolerant shared-memory abstraction to write software on top of this. For example, lock-free data structures Links to an external site., schedulers, indices etc. Another option is to to write software for CXL-based distributed memory systems Links to an external site..