More Like this

1. KnitGIST: A Programming Synthesis Toolkit for Generating Functional Machine-Knitting Textures

   https://doi.org/10.1145/3379337.3415590  

   Megan Hofmann, Jennifer Mankoff (January 2020, ACM)

   null (Ed.)

   Automatic knitting machines are robust, digital fabrication devices that enable rapid and reliable production of attractive, functional objects by combining stitches to produce unique physical properties. However, no existing design tools support optimization for desirable physical and aesthetic knitted properties. We present KnitGIST (Generative Instantiation Synthesis Toolkit for knitting), a program synthesis pipeline and library for generating hand- and machine-knitting patterns by intuitively mapping objectives to tactics for texture design. KnitGIST generates a machine-knittable program in a domain-specific programming language. 

   more » « less
2. TensorRight: Automated Verification of Tensor Graph Rewrites

   Arora, Jai; Lu, Sirui; Jain, Devansh; Xu, Tianfan; Houshmand, Farzin; Phothilimthana, Phitchaya_Mangpo; Lesani, Mohsen; Narayanan, Praveen; Murthy, Karthik_Srinivasa; Bodik, Rastislav; et al (January 2025, 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025))

   Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting. To fill this gap, we introduce TensorRight, the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, TensorRight DSL, to represent rewrite rules using a novel axis definition, called aggregated-axis, which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of TensorRight DSL. TensorRight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate TensorRight’s verification capabilities by implementing rewrite rules present in XLA’s algebraic simplifier. The results demonstrate that TensorRight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic, bounded-verification system can express only 18 of these rules. 

   more » « less
3. TensorRight: Automated Verification of Tensor Graph Rewrites

   https://doi.org/10.1145/3704865  

   Arora, Jai; Lu, Sirui; Jain, Devansh; Xu, Tianfan; Houshmand, Farzin; Phothilimthana, Phitchaya Mangpo; Lesani, Mohsen; Narayanan, Praveen; Murthy, Karthik Srinivasa; Bodik, Rastislav; et al (January 2025, Proceedings of the ACM on Programming Languages)

   Tensor compilers, essential for generating efficient code for deep learning models across various applications, employ tensor graph rewrites as one of the key optimizations. These rewrites optimize tensor computational graphs with the expectation of preserving semantics for tensors of arbitrary rank and size. Despite this expectation, to the best of our knowledge, there does not exist a fully automated verification system to prove the soundness of these rewrites for tensors of arbitrary rank and size. Previous works, while successful in verifying rewrites with tensors of concrete rank, do not provide guarantees in the unbounded setting. To fill this gap, we introduce TensorRight, the first automatic verification system that can verify tensor graph rewrites for input tensors of arbitrary rank and size. We introduce a core language, TensorRight DSL, to represent rewrite rules using a novel axis definition, calledaggregated-axis, which allows us to reason about an unbounded number of axes. We achieve unbounded verification by proving that there exists a bound on tensor ranks, under which bounded verification of all instances implies the correctness of the rewrite rule in the unbounded setting. We derive an algorithm to compute this rank using the denotational semantics of TensorRight DSL. TensorRight employs this algorithm to generate a finite number of bounded-verification proof obligations, which are then dispatched to an SMT solver using symbolic execution to automatically verify the correctness of the rewrite rules. We evaluate TensorRight’s verification capabilities by implementing rewrite rules present in XLA’s algebraic simplifier. The results demonstrate that TensorRight can prove the correctness of 115 out of 175 rules in their full generality, while the closest automatic,bounded-verification system can express only 18 of these rules. 

   more » « less
4. Engineering Multifunctional Spacer Fabrics Through Machine Knitting

   https://doi.org/10.1145/3411764.3445564  

   Albaugh, Lea; McCann, James; Hudson, Scott E.; Yao, Lining (May 2021, Proceedings of the 2021 CHI Conference on Human Factors in Computing Systems (CHI '21))

   null (Ed.)

   Machine knitting is an increasingly accessible fabrication technology for producing custom soft goods. However, recent machine knitting research has focused on knit shaping, or on adapting hand-knitting patterns. We explore a capability unique to machine knitting: producing multilayer spacer fabrics. These fabrics consist of two face layers connected by a monofilament filler yarn which gives the structure stiffness and volume. We show how to vary knit patterning and yarn parameters in spacer fabrics to produce tactile materials with embedded functionality for forming soft actuated mechanisms and sensors with tunable density, stiffness, material bias, and bristle properties. These soft mechanisms can be rapidly produced on a computationally-controlled v-bed knitting machine and integrated directly into soft objects. 

   more » « less
5. Sia: Optimizing Queries using Learned Predicates

   Qi Zhou, Joy Arulraj (January 2021, SIGMOD record)

   Predicate-centric rules for rewriting queries is a key technique in optimizing queries. These include pushing down the predicate below the join and aggregation operators, or optimizing the order of evaluating predicates. However, many of these rules are only applicable when the predicate uses a certain set of columns. For example, to move the predicate below the join operator, the predicate must only use columns from one of the joined tables. By generating a predicate that satisfies these column constraints and preserves the semantics of the original query, the optimizer may leverage additional predicate-centric rules that were not applicable before. Researchers have proposed syntax-driven rewrite rules and machine learning algorithms for inferring such predicates. However, these techniques suffer from two limitations. First, they do not let the optimizer constrain the set of columns that may be used in the learned predicate. Second, machine learning algorithms do not guarantee that the learned predicate preserves semantics. In this paper, we present SIA, a system for learning predicates while being guided by counter-examples and a verification technique, that addresses these limitations. The key idea is to leverage satisfiability modulo theories to generate counter-examples and use them to iteratively learn a valid, optimal predicate. We formalize this problem by proving the key properties of synthesized predicates. We implement our approach in SIA and evaluate its efficacy and efficiency. We demonstrate that it synthesizes a larger set of valid predicates compared to prior approaches. On a collection of 200 queries derived from the TPC-H benchmark, SIA successfully rewrites 114 queries with learned predicates. 66 of these rewritten queries exhibit more than 2X speed up. 

   more » « less