Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Optimal Software Pipelining using an SMT-Solver

Jan-Willem Roorda

TL;DR

The paper tackles the problem of generating optimal software-pipelined schedules for loops on VLIW processors, an NP-complete challenge for which prior work relied on heuristics. It introduces an SMT-based framework that encodes modulo scheduling with variables for operation cycles, slot usage, and data routing, and extends it with a lazy, incremental register-pressure model to ensure feasible allocations. Empirical results on 400+ loops across two generations of VLIW cores show the SMT approach yields better schedules than heuristics in most cases (max speed-up 1.22; geometric mean 1.08) and provides useful unsat-core feedback to diagnose infeasibility. The work demonstrates both the practicality and value of exact scheduling in compiler design, while outlining future enhancements such as symmetry-breaking to reduce search space.

Abstract

Software Pipelining is a classic and important loop-optimization for VLIW processors. It improves instruction-level parallelism by overlapping multiple iterations of a loop and executing them in parallel. Typically, it is implemented using heuristics. In this paper, we present an optimal software pipeliner based on a Satisfiability Modulo Theories (SMT) Solver. We show that our approach significantly outperforms heuristic algorithms and hand-optimization. Furthermore, we show how the solver can be used to give feedback to programmers and processor designers on why a software pipelined schedule of a certain initiation interval is not feasible.

Optimal Software Pipelining using an SMT-Solver

TL;DR

The paper tackles the problem of generating optimal software-pipelined schedules for loops on VLIW processors, an NP-complete challenge for which prior work relied on heuristics. It introduces an SMT-based framework that encodes modulo scheduling with variables for operation cycles, slot usage, and data routing, and extends it with a lazy, incremental register-pressure model to ensure feasible allocations. Empirical results on 400+ loops across two generations of VLIW cores show the SMT approach yields better schedules than heuristics in most cases (max speed-up 1.22; geometric mean 1.08) and provides useful unsat-core feedback to diagnose infeasibility. The work demonstrates both the practicality and value of exact scheduling in compiler design, while outlining future enhancements such as symmetry-breaking to reduce search space.

Abstract

Software Pipelining is a classic and important loop-optimization for VLIW processors. It improves instruction-level parallelism by overlapping multiple iterations of a loop and executing them in parallel. Typically, it is implemented using heuristics. In this paper, we present an optimal software pipeliner based on a Satisfiability Modulo Theories (SMT) Solver. We show that our approach significantly outperforms heuristic algorithms and hand-optimization. Furthermore, we show how the solver can be used to give feedback to programmers and processor designers on why a software pipelined schedule of a certain initiation interval is not feasible.
Paper Structure (21 sections, 5 figures)

This paper contains 21 sections, 5 figures.

Table of Contents

  1. Introduction
  2. VLIW
  3. Compiling for VLIW
  4. Loop Unrolling
  5. Software Pipelining
  6. Implementations of Software pipelining
  7. SAT and SMT
  8. Our contribution
  9. Example of the use of the UNSAT-core
  10. Description
  11. Modulo Scheduling
  12. the SMT Problem for SWP
  13. The exhaustive algorithm
  14. Extending the algorithm with Register Pressure
  15. Extension of the SMT Problem to deal with Register Pressure
  16. ...and 6 more sections

Figures (5)

  • Figure 1:
  • Figure 2:
  • Figure 3:
  • Figure 4: An example of an unsatisfiable core.
  • Figure 5: