Looking for project partners? Want to discuss ideas? Here's your place.
Looking for at least one Partner
We have two conflicting ideas in our team and I am looking if anyone (at least one person to form a group of two, if not three) is interested to switch teams in the last minute to work with me on verification of software transactional memory, focused on the Rochester STM (RSTM). I will briefly describe what people have already done and then describe what can be done in this project.
Verification of safety (strict serializability, abort consistency), liveness (live-lock free, etc.)
One paper has taken old STMs like DSTM, TL2 where they could reduce the problem of verifying serializability for an arbitrary number of threads with arbitrary number of shared variables to that of 2 threads with 2 shared variables from which they could successfully build a transition system and verify. Two other papers took other STMs (SigTM and also TL2) and verified only a subset of the problem - 2 threads, each with 1 transaction with at most 3 reads/writes to shared variables and no non-transactional operations. There were similar results for liveness properties. No one explored RSTM till now.
What can be done
To start off, we can consider the same small subset of 2 threads, each with 1 transaction with at most 3 reads/writes to shared variables and no non-transactional operations which helps us bound everything and build a transition system and verify safety properties - this will become the first model checking of RSTM ever. If we get some great ideas, we can also extend it to more number of threads - if we cannot generalize to arbitrary number of threads, we can at least go upto 8 or 16 which is good enough I believe.
There is a much more interesting idea on the liveness side. As RSTM only guarantees live-lock freedom "practically", we might study the patterns of transactions for some benchmarks and prove a bound on the probability of live-lock freedom using "statistical model checking" (SMC). SMC works by checking the liveness on simulation traces (I have just built such a tool for my research) and infers the probability using hypothesis testing.
Anvesh Komuravelli email: firstname.lastname@example.org phone: 217-778-3170
- Scan through the papers at this year's SOSP (2009) and mine for further work or brokenness!
- RDMA meets trusted computing meets client/server function partitioning
- Many topics in multicore
- Operating system support for multicore - is barrelfish right? wrong?
- Cache management in multicore systems - see Silas @ MIT work, talk to dga for more info.
- How to use cores? How to allocate OS functionality across cores? (See SOSP 2009 paper on RouteBricks to see an example of this idea applied to building a high-performance router on a modern multicore architecture)
- How to use cores to improve X, for X in (security, reliability, ease of use, latency hiding, usability)
- Operating system and distributed system support for robotics: The Intel research robot "Herb" faces a design challenge: How much computing to use on-board, how much to place offboard accessible via wireless. How to balance the placement of function between these two areas. (Warning: dga knows nothing about robots; project in consultation with Sidd at Intel.)
- Systems energy management in the Intel robot (as above)
- Error reporting in the Perspectives system for SSL certificate verification. How can the system detect, monitor, diagnose, and report potential SSL attacks?
- Bug mining: Find commits to repositories that appear to change off-by-one or similar errors; search for similar/same changes in other repositories to automatically detect bugs in large sets of code.
- Create a citeseer-like system running on the FAWN cluster (fast array of wimpy nodes -- energy efficient cluster architecture on wimpy embedded systems)
- Create and evaluate a general purpose interface for reporting transmit delay of packets sent via the network (useful for NTP, network monitoring, etc.).
- Generalized RDMA without trust: Efficient packet matching and dispatching code into the device (state machine? etc.; dga has some ideas) for being able to offload protocols to the NIC without extending full trust.
- Intrusion detection / virus scanning programs often need to interpose or intercept data that "belongs" to the browser (html, activex, etc.). Generic mechanism for letting / forcing content-downloading/browsing programs to interpose on these things? (Requires windows experience, likely.); idea: David Brumley
- Better badder MapReduce / Dryad improvements for cluster data analytics.
- Creating a benchmark for modern data-intensive workloads (in consultation with industry).
The A-team: Athula Balachandran, Wolf Richter, and Erik Zawadzki
Search Algorithms on a Cluster: Chris Martens, Michelle Mazurek, David Renshaw.
Speed Bumps: Ligia Nistor, Olatunji Ruwase, and James Tolbert
YTBN: Anvesh Komuravelli, Srivatsan Narayanan, Vivek Seshadri
General Packets: Yoshi Abe, Hyeontaek Lim
RDMA Extension: Anshul Madan, Chris Fallin, Filipe Militao
Hadoop & Dryad: Karan Handa, Junli Xian, Reinhard Munz
Link to 712_Project_Meeting
Link to 712_Final_Presentations