31 October 2000

Austin, TX, USA

(pre-FMCAD2000 Workshop)

The purpose of this workshop is to discuss formal specification and verification techniques
for shared memory systems. Verification of shared memory behavior (whether concurrent reads,
writes, fences, and synchronization operations issued to shared locations behave as expected) is a
problem of critical importance for microprocessor manufacturers.  Current verification methods
based on test suites are often applied very late in the design cycle and are often inconclusive.  To add
to the complexity, violating executions are not very easily discernible. Coherency protocols are
exceedingly complex and subject to many revisions.  A  recent challenge problem further illustrates
the difficulty of verifying shared memory systems. Similar problems occur in other (related) areas
also.

Papers in any of these (or related) topics are solicited:

- how to unambiguously specify the ordering rules for loads, stores, various flavors of fences,
   and other synchronization operations.
- how to formally compare different memory models and alternate definitions of the same model
- how to detect ordering violations in verification and simulation models effectively
- how to design coherence protocols through systematic goal-driven refinement to
    respect a given set of ordering rules
- how to capture manual design steps for effective use in formal verification
- how to manage the complexity of formal verification of shared memory systems
- case studies of formal design, specification, and verification techniques of shared memory
   systems and coherence protocols

WORKSHOP DETAILS (Subject to revision):

The format of the workshop will be as follows:

 * Proceedings: There will be a participants' edition of the proceedings.

  * INVITED TALKS:
       - W.W. Collier (Multiprocessor Diagnostics)
       - Xiaowei Shen and Arvind    (MIT)
       - Gil Neiger (Intel)
       - Bill Pugh (Univ of Maryland) - Memory Models for Programming Languages
       - Yuan Yu, Mark Tuttle (Compaq) - Analyzing Cache Coherence with TLA+

LINK TO PAPERS

  * ADVANCE PROGRAM (all timings subject to revision; talks may be reordered too)

    8.30   -    9.20   : Invited talk: W.W. Collier (Multiprocessor Diagnostics)
                              Overview of ARCHTEST

    9.20   -  10.10   : Invited talk: Arvind and Xiaowei Shen (MIT),
                              Design and Verification of Adaptive Cache Coherence Protocols

  10.10   -  10.45   : Shaz Qadeer (Compaq),
                              On the verification of memory models of shared memory multiprocessors

  10.45   -  11.00   : Coffee break

  11.00   -  11.50   : Invited talk: Yuan Yu and Mark Tuttle (Compaq)
                               Analyzing Cache Coherence with TLA+

  11.50   -  12.25   : Marius Laza, Rita Sharma, Anne Condon, and Alan Hu (UBC)
                              Protocols for which proving sequential consistency is easy

  12.25   -    2.00   : Lunch - catered

    2.00   -    2.35   : Ganesh Gopalakrishnan (Utah), Ratan Nalumasu (HP), and Rajnish Ghughal (Intel),
                               An Overview of Test Model-Checking for Verifying Conformance to Shared Memory Models

    2.35   -    2.55  : Michael Jones (Utah),
                              A Case-Study of Test Model-Checking and Parameterized Verification on the
MIT Hierarchical Caching Network Protocol

    2.55   -    3.10  : Coffee Break

    3.10   -    4.00  : Invited talk: Bill Pugh (Maryland),
                              Memory Models for Programming Languages

    4.00   -    4.50  : Invited talk: Gil Neiger (Intel),
                              A Taxonomy of Memory Ordering Models

    4.50   -    5.30  : Lisa Higham (Calgary), Processor Coordination on Weak Memory Consistency Models

 WORKSHOP VENUE:
     The workshop will be held all day on October 31 (day prior to FMCAD'2000 - a premier forum for
     dissemination of research in applied  formal methods for the computer aided design of hardware and
     software.) The workshop will be held at Austin's Marriott at the Capitol  - the same venue as for
     FMCAD'2000. Attendees to the MPV workshop are encouraged to take advantage of this co-location
     as well as conference hotel, which has guaranteed the FMCAD00 rate for the night of Oct 30 also.

WEBSITE:
 www.cs.utah.edu/mpv

ORGANIZING COMMITTEE (subject to change):
    Ching-Tsun Chou             Intel Corporation
    Rajnish Ghughal                Intel Corporation
    Ganesh Gopalakrishnan    Univ of Utah
    Alan Hu                           Univ of British Columbia
    Paul  Loewenstein            SUN Microsystems
    Ratan Nalumasu               HP
    Shaz Qadeer                    Compaq (Palo Alto)
    Sriram Rajamani              Microsoft Research
--