Conflict-Driven Synthesis for Layout Engines

Conflict-Driven Synthesis for Layout Engines
复制标题

布局引擎的冲突驱动综合

DOI:
10.1145/3591246
复制
发表时间:
2023
影响因子:
--
通讯作者:
Bodik, Rastislav
Bodik, Rastislav
中科院分区:
--
文献类型:
--
作者:
Liu, Junrui;Chen, Yanju;Atkinson, Eric;Feng, Yu;Bodik, Rastislav

文献摘要

参考文献

相似文献

现代Web浏览器依赖于布局引擎将HTML文档转换为指定颜色、大小和位置的布局树。然而,由于Web标准的复杂性,现有的布局引擎非常难以维护。这是尤其如此的增量布局引擎,这是为了提高性能,只更新的布局树的部分,需要被changed.In本文中,我们提出了Medea,一个新的框架自动生成增量布局引擎。Medea将布局引擎的规范与增量实现分离,通过布局引擎综合来保证布局引擎的正确性。合成是由一个新的迭代算法的基础上检测冲突,防止增量algorithm.We的最优性评估Medea的HTML布局,包括具有挑战性的功能,如边距折叠,浮动布局,和绝对定位的片段。美狄亚成功地为这个片段合成了一个增量布局引擎。该综合布局引擎既正确又高效。特别是,我们演示了它避免了Chrome、Firefox和Safari的布局引擎中报告的真实错误。Medea合成的增量布局引擎比原始增量基线快1.82倍。我们还证明了我们的冲突驱动算法产生的引擎比没有冲突分析的基线快2.74倍。
Modern web browsers rely on layout engines to convert HTML documents to layout trees that specify color, size, and position. However, existing layout engines are notoriously difficult to maintain because of the complexity of web standards. This is especially true for incremental layout engines, which are designed to improve performance by updating only the parts of the layout tree that need to be changed.In this paper, we propose Medea, a new framework for automatically generating incremental layout engines. Medea separates the specification of the layout engine from its incremental implementation, and guarantees correctness through layout engine synthesis. The synthesis is driven by a new iterative algorithm based on detecting conflicts that prevent optimality of the incremental algorithm.We evaluated Medea on a fragment of HTML layout that includes challenging features such as margin collapse, floating layout, and absolute positioning. Medea successfully synthesized an incremental layout engine for this fragment. The synthesized layout engine is both correct and efficient. In particular, we demonstrated that it avoids real-world bugs that have been reported in the layout engines of Chrome, Firefox, and Safari. The incremental layout engine synthesized by Medea is up to 1.82× faster than a naive incremental baseline. We also demonstrated that our conflict-driven algorithm produces engines that are 2.74× faster than a baseline without conflict analysis.
使用基于搜索的技术自动修复跨浏览器布局问题
DOI: 10.1145/3092703.3092726
发表时间: 2017
期刊: Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis
影响因子: --
作者:
Sonal Mahajan;Abdulmajeed Alameer;Phil McMinn;William G. J. Halfond
通讯作者: William G. J. Halfond
DOI: 10.1109/ase.2015.31
发表时间: 2015
期刊: 2015 30th IEEE/ACM International Conference on Automated Software Engineering (ASE)
影响因子: --
作者:
Thomas A. Walsh;Phil McMinn;Gregory M. Kapfhammer
通讯作者: Gregory M. Kapfhammer
Smten 具有基于可满足性的搜索
DOI: 10.1145/2714064.2660208
发表时间: 2014
影响因子: --
作者:
R. Uhler;Nirav H. Dave
通讯作者: Nirav H. Dave
针对异构树的健全、细粒度的遍历融合
DOI: 10.1145/3314221.3314626
发表时间: 2019
期刊: 40th ACM SIGPLAN Conference on Programming Language Design and Implementation
影响因子: --
作者:
Sakka, Laith;Sundararajah, Kirshanthan;Newton, Ryan R.;Kulkarni, Milind
通讯作者: Kulkarni, Milind
DOI: 10.1145/3296979.3192382
发表时间: 2017-11
影响因子: --
作者:
Yu Feng;R. Martins;O. Bastani;Işıl Dillig
通讯作者: Yu Feng;R. Martins;O. Bastani;Işıl Dillig