There is a growing overlap between PLDI and ISCA, and this workshop is convened to bring together people in that overlap. The subject coverage would be supporting ISCA-style hardware development via new programming languages, compilers, formal-verification tools, synthesis approaches, and so forth. Architecture is a relatively stodgy area, especially in industry, when it comes to adoption of new tools, and we would aim to provide a little more of a nudge to architects to try new tools, while also exposing PL experts to challenges they may not have been aware of in an adjacent community. More keywords of high interest lately to both communities include security (including side channels), weak memory models, testing, debugging, optimization, and hardware-software codesign. General approaches already being considered across this disciplinary boundary include domain-specific languages (embedded or freestanding), metaprogramming, partial evaluation, SMT solvers, proof assistants, model checking, symbolic execution, type systems, and mechanized semantics.

Thanks for a great event! Videos of most presentations are now available on YouTube.

Plenary
You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 17 Jun

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

07:30 - 09:00
BreakfastCatering at Royal
07:30
90m
Other
Breakfast
Catering

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
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 / AWS, Adam Chlipala Massachusetts Institute of Technology
11:00 - 11:20
11:00
20m
Coffee break
Break
Catering

11:20 - 12:30
PLARCH: Session 2PLARCH at Magnolia 4
Chair(s): Mengjia Yan MIT

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

11:20
10m
Talk
Tags: A Framework for Distributed Event Ordering
PLARCH
Paul Mure Stanford University, Nathan Zhang Stanford University, Caroline Trippel Stanford University, Kunle Olukotun Stanford University
11:30
15m
Talk
Stellar: A DSL to Build and Explore Sparse Accelerators
PLARCH
Hasan Genc UC Berkeley, Hansung Kim University of California, Berkeley, Prashanth Ganesh University of California, Berkeley, Yakun Sophia Shao University of California, Berkeley
11:45
15m
Talk
PEak: A Single Source of Truth for Hardware Design and Verification
PLARCH
Caleb Donovick Stanford University, Ross Daly Stanford University, USA, Jackson Melchert Stanford University, Leonard Truong Stanford University, Priyanka Raina Stanford University, Pat Hanrahan Stanford University, USA, Clark Barrett Stanford University
12:00
10m
Talk
Challenges with Hardware-Software Co-design for Sparse Machine Learning on Streaming Dataflow
PLARCH
Rubens Lacouture Stanford University, Olivia Hsu Stanford University, Kunle Olukotun Stanford University, Fredrik Kjolstad Stanford University
12:30 - 14:00
LunchCatering at Royal
12:30
90m
Lunch
Lunch
Catering

14:00 - 15:30
PLARCH: Session 3PLARCH at Magnolia 4
Chair(s): Caroline Trippel Stanford University

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

14:00
15m
Talk
They're the same picture: a software-verification flow adapted for hardware verification
PLARCH
Andreas Lööw Imperial College London, Magnus O. Myreen Chalmers University of Technology
Pre-print
14:15
15m
Talk
Design for Hardware Memory Model Verification
PLARCH
Yao Hsiao Stanford University, Yasas Seneviratne University of Virginia, Tommy Tracy II University of Virginia, Kevin Skadron University of Virginia, Caroline Trippel Stanford University
File Attached
14:40
10m
Talk
Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
PLARCH
Tianrui Wei University of California, Berkeley, Shangyin Tan University of California at Berkeley, Koushik Sen University of California at Berkeley, Krste Asanovic University of California Berkeley
14:50
10m
Talk
NFC:Next-generation Formal verification for high performance Caches
PLARCH
Tianrui Wei University of California, Berkeley, Jerry Zhao UC Berkeley, Krste Asanovic University of California Berkeley
15:00
10m
Talk
Sandia's Formal Hardware Design and Verification, Present and Future
PLARCH
Noah Evans Sandia National Laboratories
15:10
10m
Talk
Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
PLARCH
Ben Blaxill Groq, Samuel Grütter Massachusetts Institute of Technology, Jade Philipoom Google, Germany, Satnam Singh Groq
15:30 - 16:00
15:30
30m
Coffee break
Break
Catering

16:00 - 17:50
PLARCH: Session 4PLARCH at Magnolia 4
Chair(s): Adrian Sampson Cornell University

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

16:00
15m
Talk
Novel Numerical Hardware Design Methodology - From machine readable specification to optimized RTL
PLARCH
Theo Drane Intel Corporation, USA, Bill Zorn Intel Corporation, USA, Samuel Coward Imperial College London, UK / Intel Corporation
File Attached
16:15
15m
Talk
Mixed-Abstraction HDLs and A Discussion on Other Aspects of HDL Design
PLARCH
Vighnesh Iyer University of California, Berkeley, Borivoje Nikolic University of California, Berkeley
File Attached
16:30
10m
Talk
New Embedded DSLs for Hardware Design and Verification
PLARCH
Vighnesh Iyer University of California, Berkeley, Kevin Laeufer UC Berkeley, Young-Jin Park University of California, Berkeley, Rohit Agarwal University of California, Berkeley, Lixiang Yin University of California, Berkeley, Bryan Ngo University of California, Berkeley, Oliver Yu University of California, Berkeley, Koushik Sen University of California at Berkeley, Borivoje Nikolic University of California, Berkeley
File Attached
16:40
10m
Talk
Fearless Hardware Design
PLARCH
Rachit Nigam Cornell University
17:00
10m
Talk
Library-based Compartmentalisation on CHERI
PLARCH
Dapeng Gao University of Cambridge, Robert N. M. Watson University of Cambridge
17:10
10m
Talk
Non-Newtonian Hardware Design for Longevity
PLARCH
Guy Wilks UC Santa Barbara, Jonathan Balkind UC Santa Barbara
17:20
10m
Talk
On the Generality of Matrix Multiplication
PLARCH
Andrew Alex UC Santa Barbara, Zachary Sisco UC Santa Barbara, Jonathan Balkind UC Santa Barbara
17:30
10m
Talk
ChatGPT, Make a Secure Malloc for me
PLARCH
Jeremy Singer University of Glasgow, Zheng Wang University of Leeds, UK
Pre-print

Accepted Papers

Title
Challenges with Hardware-Software Co-design for Sparse Machine Learning on Streaming Dataflow
PLARCH
ChatGPT, Make a Secure Malloc for me
PLARCH
Pre-print
Design for Hardware Memory Model Verification
PLARCH
File Attached
Fearless Hardware Design
PLARCH
Generate Compilers from Hardware Models!
PLARCH
Goals for a modern ISA specification
PLARCH
Hardware-Software Codesign for Mitigating Spectre
PLARCH
File Attached
Hardware Verification of Timing Side Channel Freedom in the Spectre Era
PLARCH
Leakage models are a leaky abstraction: the case for cycle-level verification of constant-time cryptography
PLARCH
Pre-print
Library-based Compartmentalisation on CHERI
PLARCH
Mixed-Abstraction HDLs and A Discussion on Other Aspects of HDL Design
PLARCH
File Attached
Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
PLARCH
New Embedded DSLs for Hardware Design and Verification
PLARCH
File Attached
NFC:Next-generation Formal verification for high performance Caches
PLARCH
Non-Newtonian Hardware Design for Longevity
PLARCH
Novel Numerical Hardware Design Methodology - From machine readable specification to optimized RTL
PLARCH
File Attached
On the Generality of Matrix Multiplication
PLARCH
PEak: A Single Source of Truth for Hardware Design and Verification
PLARCH
Sandia's Formal Hardware Design and Verification, Present and Future
PLARCH
Semi-Automated Translation of a Formal ISA Specification to Hardware
PLARCH
File Attached
Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
PLARCH
Stellar: A DSL to Build and Explore Sparse Accelerators
PLARCH
Tags: A Framework for Distributed Event Ordering
PLARCH
They're the same picture: a software-verification flow adapted for hardware verification
PLARCH
Pre-print

Call for Talks

TLDR: We are collecting position papers proposing talks about big ideas and research projects (and maybe sufficiently interesting tools that are “just engineering”) within the workshop scope. There are no associated formally published papers, and we aim to encourage discussion at and after the workshop. Contributed talk slots likely won’t be longer than 30 minutes.

PLARCH’23 is co-located with both ISCA and PLDI, within the larger FCRC experience.

Submit your 2-page position paper via HotCRP. Important dates:

  • Paper submission: April 28th, 2023 (Anywhere on Earth)
  • Author Notification: May 12th, 2023
  • Workshop: June 17th, 2023

Scope. PLARCH is a venue for discussion, debate, and brainstorming at the intersection of ISCA and PLDI topics. We hope to interpret that scope broadly in creating the program. Perhaps a good fundamental rule of thumb is that a project being presented at PLARCH should include technical challenges recognizable to both architecture and programming-languages researchers, though the challenges could be significantly greater on one of those sides.

One mad lib-style recipe to generate an in-scope topic could be to settle on

  • language design, compilers, debuggers, testing tools, profilers, formal verification, (program) synthesis, …

for

  • development of computer processors, memory systems, accelerators, networking hardware, …

PLARCH is not a conference, and we’re excited to hear compelling talks in categories like:

  • Early, in-progress research snapshots
  • Experience reports
  • Essays advocating for or against a general approach
  • Retrospectives on past efforts
  • Calls for solutions to open challenges in the area (questions without answers)
  • Demonstrations of real systems (to be shown off in live demos at the workshop)

Position Papers

The primary goal of the workshop is to enable discussion. It will accept 2-page position papers. The workshop will allocate short time slots to the papers, each paired with a discussion following SNAPL’s discussion format: “table discussion” where small breakout groups will discuss the paper, followed by plenary Q&A.

Position paper submissions will undergo peer review by a program committee of interdisciplinary experts working on both high-level (languages, compilers, drivers) and low-level (circuit optimization, interconnect design) problems in the area.

Formatting. Papers should use the two-column the formatting guidelines for SIGPLAN conferences (the acmart format with the sigplan two-column option) and not exceed 2 pages, excluding references. Review is single-blind, so please include authors’ names on the submitted PDF.

Paper submission will is via HotCRP. The accepted papers will not be published in a proceedings—PDFs will instead appear on the workshop’s website.

Important guidelines. It’s standard for papers to start with a general motivation: Moore’s Law is doomed; specialized hardware is ascendant; Verilog is hard to use; etc. Please skip this part in your PLARCH position paper (and in eventual talks at the workshop). The PLARCH audience will already believe these things, so save the space & time and instead focus on your own unique ideas. As much as possible, dispose with the framing and motivation so you can focus on the technical content.

Remember that the goal at PLARCH is to stimulate discussion, not to disseminate fully polished results. So don’t be afraid to write up half-baked ideas and in-progress work: it’s OK if your submission has zero bar charts, for example.

For examples of past position papers, consider looking at the programs for LATTE’22 and ’21.

Credit: much of this call is cribbed from a LATTE call!