PLDI 2023
Sat 17 - Wed 21 June 2023 Orlando, Florida, United States
PLDI 2023 (series) / PLARCH 2023 (series) / Programming Languages for Architecture /

Goals for a modern ISA specification

PLARCH 2023
Sat 17 Jun 2023 09:00 - 09:15 at Magnolia 4 - PLARCH: Session 1 Chair(s): Adam Chlipala

What should you consider if you are creating an ISA specification in 2023? What uses matter? What are the quality goals? How should we build the specification and what tools do we need? What is in scope and what is out of scope? What can we learn from existing machine readable specifications?

Researcher at Arm Ltd (UK) since 2004

  • model checking processor pipelines (newest)
  • formal architecture specifications
  • wide SIMD instruction set
  • pipeline parallelism
  • software defined radio
  • vectorising compilers (oldest)

Researcher at University of Utah (USA), 1998-2004

  • component based operating system kernels

Researcher at Yale University (USA), 1994-1998

  • Haskell foreign function interface
  • Functional Reactive Programming
  • Visual Tracking in Haskell
  • Haskell library/compiler development

Researcher at University of Glasgow (UK), 1988-1994

  • Formal Specification and Verification
  • GHC foreign function interface

Sat 17 Jun

Displayed time zone: Eastern Time (US & Canada) change

09:00 - 11:00
PLARCH: Session 1PLARCH at Magnolia 4
Chair(s): Adam Chlipala Massachusetts Institute of Technology

#plarch-sat-magnolia4 Discord icon small YouTube icon small

09:00
15m
Talk
Goals for a modern ISA specification
PLARCH
Alastair Reid Arm Ltd
09:25
15m
Talk
Generate Compilers from Hardware Models!
PLARCH
Gus Henry Smith University of Washington, Benjamin Kushigian University of Washington, Vishal Canumalla University of Washington, Andrew Cheung University of Washington, René Just University of Washington, Zachary Tatlock University of Washington
09:40
10m
Talk
Semi-Automated Translation of a Formal ISA Specification to Hardware
PLARCH
Harlan Kringen UC Santa Barbara, Zachary Sisco UC Santa Barbara, Jonathan Balkind UC Santa Barbara, Timothy Sherwood University of California at Santa Barbara, Ben Hardekopf University of California at Santa Barbara
File Attached
10:00
15m
Talk
Leakage models are a leaky abstraction: the case for cycle-level verification of constant-time cryptography
PLARCH
Anish Athalye MIT, M. Frans Kaashoek Massachusetts Institute of Technology, USA, Nickolai Zeldovich Massachusetts Institute of Technology, USA, Joseph Tassarotti NYU
Pre-print
10:15
15m
Talk
Hardware-Software Codesign for Mitigating Spectre
PLARCH
Nicholas Mosier Stanford University, Kate Eselius Stanford University, Hamed Nemati Stanford University, CISPA Helmholtz Center for Information Security, John C. Mitchell Stanford University, Caroline Trippel Stanford University
File Attached
10:30
15m
Talk
Hardware Verification of Timing Side Channel Freedom in the Spectre Era
PLARCH
Stella Lau MIT CSAIL, Thomas Bourgeat MIT CSAIL, Clément Pit-Claudel EPFL, Adam Chlipala Massachusetts Institute of Technology
Alastair Reid

Alastair Reid

Arm Ltd