PLDI 2023
Sat 17 - Wed 21 June 2023 Orlando, Florida, United States
PLDI 2023 (series) / Orlando World Center Marriott /

Room information: Magnolia 4

VenueOrlando World Center Marriott
Room nameMagnolia 4
Room InformationNo extra information available
Program

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

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

Sun 18 Jun

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

09:00 - 11:00
CTSTA: Session 1CTSTA at Magnolia 4

#ctsta-sun-magnolia4 Discord icon small YouTube icon small

09:00
5m
Day opening
Introduction
CTSTA
Fredrik Kjolstad Stanford University
09:05
15m
Talk
Software and Hardware for Sparse ML
CTSTA
Fredrik Kjolstad Stanford University
09:20
15m
Talk
Integrating Data Layout into Compilers and Code Generators
CTSTA
Mary Hall University of Utah
09:35
15m
Talk
Tackling the challenges of high-performance graph analytics at compiler level
CTSTA
Gokcen Kestor Pacific Northwest National Laboratory
09:50
10m
Panel
Discussion
CTSTA

10:00
5m
Break
BreakSocial
CTSTA

10:05
15m
Talk
Challenges and Opportunities for Sparse Compilers in LLM
CTSTA
Zihao Ye University of Washington
10:20
15m
Talk
The Sparse Abstract Machine
CTSTA
Olivia Hsu Stanford University
10:35
15m
Talk
TeAAL: A Declarative Framework for Modeling Sparse Tensor Accelerators
CTSTA
Nandeeka Nayak University of Illinois at Urbana-Champaign
10:50
10m
Panel
Discussion
CTSTA

11:20 - 12:30
CTSTA: Session 2CTSTA at Magnolia 4

#ctsta-sun-magnolia4 Discord icon small YouTube icon small

11:20
15m
Talk
Accelerating Sparse Matrix Computations with Code Specialization
CTSTA
Maryam Mehri Dehnavi University of Toronto
11:35
15m
Talk
A General Distributed Framework for Contraction of a Sparse Tensor with a Tensor Network
CTSTA
Raghavendra Kanakagiri University of Illinois Urbana-Champaign
11:50
15m
Talk
Automatic Differentiation for Sparse TensorsVirtual
CTSTA
Amir Shaikhha University of Edinburgh
12:05
15m
Talk
Compiler Support for Structured Data
CTSTA
Saman Amarasinghe Massachusetts Institute of Technology
12:20
10m
Panel
Discussion
CTSTA

14:00 - 15:30
CTSTA: Session 3CTSTA at Magnolia 4

#ctsta-sun-magnolia4 Discord icon small YouTube icon small

14:00
15m
Talk
Learning workload-aware cost model for sparse tensor program
CTSTA
Jaeyeon Won Massachusetts Institute of Technology
14:15
15m
Talk
Autoscheduling for Sparse Tensor Contraction
CTSTA
Kirshanthan Sundararajah Purdue University
14:30
10m
Panel
Discussion
CTSTA

14:40
15m
Talk
Fantastic Sparse Masks and Where to Find Them
CTSTA
Shiwei Liu The University of Texas at Austin, Texas, USA
14:55
15m
Talk
Moving the MLIR Sparse Compilation Pipeline into ProductionVirtual
CTSTA
Aart Bik Google, Inc., Peiming Liu Google Inc
15:10
15m
Panel
Discussion
CTSTA

15:25
5m
Day closing
Closing
CTSTA
Fredrik Kjolstad Stanford University, Saman Amarasinghe Massachusetts Institute of Technology
16:00 - 17:50
CTSTA: Session 4CTSTA at Magnolia 4

#ctsta-sun-magnolia4 Discord icon small YouTube icon small

16:00
1h50m
Poster
Poster Session and Free-Form Discussion
CTSTA

Sat 17 Jun

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Magnolia 4

PLARCH

PLARCH: Session 1

PLARCH

PLARCH: Session 2

PLARCH

PLARCH: Session 3

PLARCH

PLARCH: Session 4

Sun 18 Jun

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

Room9:003010:003011:003012:003013:003014:003015:003016:003017:0030
Magnolia 4

CTSTA

CTSTA: Session 1

CTSTA

CTSTA: Session 2

CTSTA

CTSTA: Session 3

CTSTA

CTSTA: Session 4

Sat 17 Jun

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Magnolia 4
PLARCH
Goals for a modern ISA specification
09:00 - 09:15
PLARCH
Generate Compilers from Hardware Models!
09:25 - 09:40
PLARCH
Semi-Automated Translation of a Formal ISA Specification to Hardware
09:40 - 09:50
PLARCH
Leakage models are a leaky abstraction: the case for cycle-level verifi ...
10:00 - 10:15
PLARCH
Hardware-Software Codesign for Mitigating Spectre
10:15 - 10:30
PLARCH
Hardware Verification of Timing Side Channel Freedom in the Spectre Era
10:30 - 10:45
PLARCH
Tags: A Framework for Distributed Event Ordering
11:20 - 11:30
PLARCH
Stellar: A DSL to Build and Explore Sparse Accelerators
11:30 - 11:45
PLARCH
PEak: A Single Source of Truth for Hardware Design and Verification
11:45 - 12:00
PLARCH
Challenges with Hardware-Software Co-design for Sparse Machine Learning ...
12:00 - 12:10
PLARCH
They're the same picture: a software-verification flow adapted for hard ...
14:00 - 14:15
PLARCH
Design for Hardware Memory Model Verification
14:15 - 14:30
PLARCH
Nerv: Probabilistic Dynamic Partial Order Reduction for Hardware
14:40 - 14:50
PLARCH
NFC:Next-generation Formal verification for high performance Caches
14:50 - 15:00
PLARCH
Sandia's Formal Hardware Design and Verification, Present and Future
15:00 - 15:10
PLARCH
Silver Oak: Hardware Software Co-Design and Co-Verification in Coq
15:10 - 15:20
PLARCH
Novel Numerical Hardware Design Methodology - From machine readable spe ...
16:00 - 16:15
PLARCH
Mixed-Abstraction HDLs and A Discussion on Other Aspects of HDL Design
16:15 - 16:30
PLARCH
New Embedded DSLs for Hardware Design and Verification
16:30 - 16:40
PLARCH
Fearless Hardware Design
16:40 - 16:50
PLARCH
Library-based Compartmentalisation on CHERI
17:00 - 17:10
PLARCH
Non-Newtonian Hardware Design for Longevity
17:10 - 17:20
PLARCH
On the Generality of Matrix Multiplication
17:20 - 17:30
PLARCH
ChatGPT, Make a Secure Malloc for me
17:30 - 17:40

Sun 18 Jun

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

Room9:0015304510:0015304511:0015304512:0015304513:0015304514:0015304515:0015304516:0015304517:00153045
Magnolia 4
CTSTA
Introduction
09:00 - 09:05
CTSTA
Software and Hardware for Sparse ML
09:05 - 09:20
CTSTA
Integrating Data Layout into Compilers and Code Generators
09:20 - 09:35
CTSTA
Tackling the challenges of high-performance graph analytics at compiler ...
09:35 - 09:50
CTSTA
Discussion
09:50 - 10:00
CTSTASocial
Break
10:00 - 10:05
CTSTA
Challenges and Opportunities for Sparse Compilers in LLM
10:05 - 10:20
CTSTA
The Sparse Abstract Machine
10:20 - 10:35
CTSTA
TeAAL: A Declarative Framework for Modeling Sparse Tensor Accelerators
10:35 - 10:50
CTSTA
Discussion
10:50 - 11:00
CTSTA
Accelerating Sparse Matrix Computations with Code Specialization
11:20 - 11:35
CTSTA
A General Distributed Framework for Contraction of a Sparse Tensor with ...
11:35 - 11:50
CTSTAVirtual
Automatic Differentiation for Sparse Tensors
11:50 - 12:05
CTSTA
Compiler Support for Structured Data
12:05 - 12:20
CTSTA
Discussion
12:20 - 12:30
CTSTA
Learning workload-aware cost model for sparse tensor program
14:00 - 14:15
CTSTA
Autoscheduling for Sparse Tensor Contraction
14:15 - 14:30
CTSTA
Discussion
14:30 - 14:40
CTSTA
Fantastic Sparse Masks and Where to Find Them
14:40 - 14:55
CTSTAVirtual
Moving the MLIR Sparse Compilation Pipeline into Production
14:55 - 15:10
CTSTA
Discussion
15:10 - 15:25
CTSTA
Closing
15:25 - 15:30
CTSTA
Poster Session and Free-Form Discussion
16:00 - 17:50