| United States Worldwide |
|
| United States Worldwide |
|
Sun Labs Scalable Synchronization Research GroupWe don't play transactional memory pioneers on TV, we just are them in real life.StaffDave Dice, full-time memberMaurice Herlihy, visiting professor Yossi Lev, intern ('04 - '08) Victor Luchangco, full-time member Mark Moir, Principal Investigator Kevin Moore, full-time member Dan Nussbaum, full-time member Marek Olszewski, intern ('08) Nir Shavit, part-time member AlumniAlexandra Fedorova, intern ('03 - '06)Ori Shalev, intern ('04 - '06) Virendra Marathe, intern (summer '04) Simon Doherty, intern (summer '03) Bill Scherer, intern (summer '02) PublicationsMissionThe Sun Labs Scalable Synchronization Research Group is exploring
hardware and software mechansisms for facilitating the easy
development of correct, efficient, and scalable concurrent programs.
Today's lock-based concurrent programs suffer a host of problems
including lack of composability, difficult granularity tradeoffs,
complications arising from deadlock avoidance, etc. With the advent
of multicore computing, the problem is about to become much worse,
because many more programmers will need to develop concurrent programs
in order to exploit advances in technology. News and events
Transactional MemoryWe believe that a different programming model is needed to support widespread effective development of concurrent programs that are correct, efficient, and scalable, and we have been exploring Transactional Memory towards that end. Recently, numerous other research groups have come to the same conclusion, and there is lots of work on transactional memory.Members of our group have pioneered research on transactional memory. Maurice Herlihy (Visiting Professor) was one of the original inventors of transactional memory and proposed the first Hardware Transactional Memory design. Nir Shavit was one of the original inventors of Software Transactional Memory. Our group has continued to contribute substantially to this area:
Other ProjectsIn addition to our focus on transactional memory support, we also work on a number of other issues related to concurrency and synchronization. By exploring various models of computing, we gain insight into what can be achieved with current hardware support, what fundamental limitations exist, and what can be achieved with various hypothetical forms of future support for synchronization. We are also very interested in techniques for proving algorithms correct, and in how various forms of synchronization support influence the difficulty of doing so. Below we briefly highlight some of these areas of investigation. See also our complete list of publications.Non-blocking Progress ConditionsWe have identified a new non-blocking progress condition: obstruction-freedom. Obstruction freedom is weaker than traditional progress conditions for non-blocking data structures, admitting substantially simpler and more efficient implementations. Modular contention managers compensate for weaker progress guarantees without affecting correctness. See our ICDCS 2003, PODC 2003 and DISC 2005 papers.Non-blocking Memory ManagementWithout locks, it is difficult to ensure objects are not accessed after being freed. Lock-Free Reference Counting showed how to do it using DCAS (double compare-and-swap). However, DCAS is not generally available. We have designed a more general and efficient approach that uses CAS, resulting in the first dynamic-sized non-blocking data structures in which process failures cannot cause unbounded memory leaks. See our TOCS 2004 paper.Double Compare-and-SwapWe have investigated what could be achieved if hardware provided a double compare-and-swap (DCAS) instruction that could atomically modify two memory locations. We found that, while DCAS enables a number of neat tricks, it is not silver bullet for nonblocking synchronization. We conclude that something stronger is needed. Something like transactional memory! See our SPAA 2004 paper.Mostly Nonblocking Data StructuresWe have recently been exploring data structure implementations that provide most of the benefits of nonblocking data structures, but make careful use of blocking to substanbtially simplify the implementation. See our LazyList algorithm described in our OPODIS 2005 paper.Formal VerificationWe are interested in formal verification of the kinds of algorithms we design. See our FORTE 2004 and CAV 2006 papers.Many Other ProjectsThe above is just a sampling of our work. See our full list of publications. | ||||||||||||||||||||||