Conflict-Driven Synthesis for Layout Engines
summary
Medea synthesizes incremental layout engines from an attribute grammar specification plus a traversal sketch, using symbolic execution to produce concrete schedules and a novel conflict-driven synthesis loop that learns conflict clauses to prune inefficient candidates. It implements dirty bits grouping for incremental updates, supports margin collapse, floats, and absolute positioning, connects synthesized engines to a browser, fixes 30 of 31 real-world layout bugs, and yields up to 1.82× speedup over a naive incremental baseline and 2.74× over a non-conflict baseline.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:23Modern layout challenges
- 3:09Layout correctness with grammars
- 7:07Domain-specific language for layout programs
- 10:40Incremental evaluation
- 12:27Synthesis procedure
- 14:52Implementation and evaluation
- 16:16Summary
- 16:38Q&A
related talks
30mAutomated High-Level Synthesis Design Modularization via E-Graph Anti-Unification
31mLetting users do the undecidable: lessons from program synthesis
17mSpineless Traversal for Layout Invalidation
26mProgram Synthesis Using Example Propagation
20mMISAAL: Synthesis-Based Automatic Generation of Efficient and Retargetable(…)
30mSemantics-Guided Synthesis
21mSynthesizing Formal Semantics from Executable Interpreters
24mSeamless Code Generator Synchronization in the Composition of Heterogeneous Modeli...