一句话：提出顺序感知的数据流模型以精确刻画并行 Unix 管道语义，并证明其并行化变换的正确性。
Unix shell 管道是广泛使用的组合式编程手段，但其中蕴含的数据并行性难以被安全地利用，原因在于复杂管道的语义（尤其是节点从不同输入边消费数据的顺序）缺乏精确的形式化刻画。本文提出一种用于建模并行 Unix shell 管道的数据流模型，该模型是「顺序感知」的：数据流图中每个节点从各条边消费输入的顺序对计算语义、进而对可行的并行化方式起核心作用。作者用该模型刻画利用 shell 计算中数据并行性的变换语义，并证明这些变换的正确性；同时形式化了从 Unix shell 到数据流模型、以及从数据流模型回译到并行 shell 脚本的翻译过程。模型与变换被实现为一个并行化 shell 管道系统的编译器和优化 pass，并在 47 条管道上评估了所获得的加速比。
We present a dataflow model for modelling parallel Unix shell pipelines. To accurately capture the semantics of complex Unix pipelines, the dataflow model is order-aware, i.e., the order in which a node in the dataflow graph consumes inputs from different edges plays a central role in the semantics of the computation and therefore in the resulting parallelization. We use this model to capture the semantics of transformations that exploit data parallelism available in Unix shell computations and prove their correctness. We additionally formalize the translations from the Unix shell to the dataflow model and from the dataflow model back to a parallel shell script. We implement our model and transformations as the compiler and optimization passes of a system parallelizing shell pipelines, and use it to evaluate the speedup achieved on 47 pipelines.
@article{paperbot1114,
title = {An order-aware dataflow model for parallel Unix pipelines},
author = {Shivam Handa and Konstantinos Kallas and Nikos Vasilakis and Martin C. Rinard},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {ICFP},
year = {2021},
doi = {10.1145/3473570}
}