SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand
Sat 10 Dec 2022 13:30 - 14:00 at Seminar Room LG004 - PLDI and POPL Papers Chair(s): Joxan Jaffar

Achieving peak performance in a computer system requires optimizations in every layer of the system, be it hardware or software. A detailed understanding of the underlying hardware, and especially the processor, is crucial to optimize software. One key criterion for the performance of a processor is its ability to exploit instruction-level parallelism. This ability is determined by the port mapping of the processor, which describes the execution units of the processor for each instruction.

Processor manufacturers usually do not share the port mappings of their microarchitectures. While approaches to automatically infer port mappings from experiments exist, they are based on processor-specific hardware performance counters that are not available on every platform.

We present PMEvo, a framework to automatically infer port mappings solely based on the measurement of the execution time of short instruction sequences. PMEvo uses an evolutionary algorithm that evaluates the fitness of candidate mappings with an analytical throughput model formulated as a linear program. Our prototype implementation infers a port mapping for Intel’s Skylake architecture that predicts measured instruction throughput with an accuracy that is competitive to existing work. Furthermore, it finds port mappings for AMD’s Zen+ architecture and the ARM Cortex-A72 architecture, which are out of scope of existing techniques.

Sat 10 Dec

Displayed time zone: Auckland, Wellington change

13:30 - 15:00
PLDI and POPL PapersCOVID Time Papers In Person at Seminar Room LG004
Chair(s): Joxan Jaffar National University of Singapore
13:30
30m
Talk
PMEvo: portable inference of port mappings for out-of-order processors by evolutionary optimization
COVID Time Papers In Person
Fabian Ritter Saarland University, Germany, Sebastian Hack Saarland University, Germany
Link to publication DOI
14:00
30m
Talk
Software Model-Checking as Cyclic-Proof Search
COVID Time Papers In Person
Takeshi Tsukada Chiba University, Hiroshi Unno University of Tsukuba; RIKEN AIP
Link to publication DOI
14:30
30m
Talk
SolType: Refinement Types for Arithmetic Overflow in Solidity
COVID Time Papers In Person
Bryan Tan , Benjamin Mariano The University of Texas at Austin, Texas, USA, Shuvendu K. Lahiri Microsoft Research, Işıl Dillig University of Texas at Austin, Yu Feng University of California at Santa Barbara
Link to publication DOI