Tutorial and Workshop on
Formal Specification and Verification Methods
for Shared Memory Systems

31 October 2000

Austin, TX, USA

(pre-FMCAD2000 Workshop)

  ------------------------------------------------------------------------

[Email] [Call for Papers in ASCII] [Call for Papers in Postscript] [FMCAD00
and MPV registration]
  ------------------------------------------------------------------------

INTRODUCTION:

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.

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:

  * Submissions:   Submissions of an extended abstract (around 10 pages)
are invited via an
     email attachment of a PDF file directly to mpv2000@cs.utah.edu by
September 10th. The organizing
     committee will evaluate your submission with respect to the overall
goals of the workshop. Both
     regular and poster presentations are planned.

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

  * INVITED TALKS:
       - Prof. Arvind    (MIT)
       - Dr. Gil Neiger (Intel)

  * Embedded Tutorials:  The embedded tutorial described below is currently
planned.
      Other tutorial proposals are welcome.

       - "Test model-checking  for verifying conformance to memory models,"
             by Ganesh Gopalakrishnan (Utah), Ratan Nalumasu (HP), and
Rajnish Ghughal (Intel).

                In this tutorial, the theory behind test model-checking will
be introduced, followed by
                a hands-on part in which the audience will be lead through
the creation of a model of
                a coherence protocol, and test automata for verifying
conformance to a memory model
                of choice. Reference material and software for the tutorial
will be made available <here>
                in due course.

DATES:
  Submissions of extended abstracts:                          September
5, 2000
  Notification of acceptance along with category:  September  20, 2000

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
--