Semantics and Scheduling for Machine Knitting Compilers
Semantics and Scheduling for Machine Knitting Compilers
复制标题
机器针织编译器的语义和调度
DOI：
10.1145/3592449
复制
发表时间：
2023
影响因子：
6.2
通讯作者：
McCann, James
中科院分区：
文献类型：
--
作者：
Lin, Jenny;Narayanan, Vidya;Ikarashi, Yuka;Ragan-Kelley, Jonathan;Bernstein, Gilbert;McCann, James
机器编织是一种成熟的复杂柔软物体的制造技术，公司和研究人员都开发了用于产生机器编织图案的工具。然而，机器编织对象的现有表示是不完整的(没有覆盖机器编织对象的整个领域)或过于具体(没有考虑编织指令序列之间的对称性和等价性)。这使得很难定义机器编织的正确性，更不用说验证给定程序或程序转换的正确性了。这项工作的主要贡献是针织的形式语义，针织是针织机的一种低级领域专用语言。我们通过使用所谓的栅栏缠结来实现这一点，它扩展了结理论中的概念，允许对编织程序等价性的数学定义与编织对象背后的直觉相匹配。最后，使用这种形式表示，我们证明了一系列重写规则的正确性；并演示了这些重写规则如何为高级任务(如为特定机器编译程序和优化时间/可靠性)奠定基础，同时在我们提出的语义下可证明生成相同的编织对象。通过建立正确性的形式化定义，为编织程序的编译和优化提供了坚实的基础。
Machine knitting is a well-established fabrication technique for complex soft objects, and both companies and researchers have developed tools for generating machine knitting patterns. However, existing representations for machine knitted objects are incomplete (do not cover the complete domain of machine knittable objects) or overly specific (do not account for symmetries and equivalences among knitting instruction sequences). This makes it difficult to define correctness in machine knitting, let alone verify the correctness of a given program or program transformation. The major contribution of this work is a formal semantics for knitout, a low-level Domain Specific Language for knitting machines. We accomplish this by using what we call thefenced tangle, which extends concepts from knot theory to allow for a mathematical definition of knitting program equivalence that matches the intuition behind knit objects. Finally, using this formal representation, we prove the correctness of a sequence of rewrite rules; and demonstrate how these rewrite rules can form the foundation for higher-level tasks such as compiling a program for a specific machine and optimizing for time/reliability, all while provably generating the same knit object under our proposed semantics. By establishing formal definitions of correctness, this work provides a strong foundation for compiling and optimizing knit programs.
登录
查看更多内容
Petr4：p4 数据平面的正式基础
影响因子：
--
作者：
Doenges, Ryan;Arashloo, Mina Tahmasbi;Bautista, Santiago;Chang, Alexander;Ni, Newton;Parkinson, Samwise;Peterson, Rudy;Solko-Breslin, Alaia;Xu, Amanda;Foster, Nate
通讯作者：
Foster, Nate
针织模板的计算设计
影响因子：
6.2
作者：
Jones, Benjamin;Mei, Yuxuan;Zhao, Haisen;Gotfrid, Taylor;Mankoff, Jennifer;Schulz, Adriana
通讯作者：
Schulz, Adriana
DOI：
10.1109/icra48506.2021.9562113
发表时间：
2021-05
期刊：
2021 IEEE International Conference on Robotics and Automation (ICRA)
影响因子：
--
作者：
Jenny Lin;J. McCann
通讯作者：
Jenny Lin;J. McCann
影响因子：
19
作者：
Vanessa Sanchez;K. Mahadevan;Gabrielle Ohlson;M. Graule;Michelle C. Yuen;Clark B. Teeple;James C. Weaver;J. McCann;K. Bertoldi;Robert J. Wood
通讯作者：
Vanessa Sanchez;K. Mahadevan;Gabrielle Ohlson;M. Graule;Michelle C. Yuen;Clark B. Teeple;James C. Weaver;J. McCann;K. Bertoldi;Robert J. Wood
DOI：
10.1145/3508499
发表时间：
2021-07
期刊：
ACM Transactions on Graphics (TOG)
影响因子：
--
作者：
Haisen Zhao;Max Willsey;Amy Zhu;Chandrakana Nandi;Zach Tatlock;J. Solomon;Adriana Schulz
通讯作者：
Haisen Zhao;Max Willsey;Amy Zhu;Chandrakana Nandi;Zach Tatlock;J. Solomon;Adriana Schulz