计算机系统软件顶会OSDI 2021最佳论文出炉，邢波团队研究入选( 二 )

在实际深度学习作业和轨迹驱动（trace-driven）模拟的实验中，相比于SOTA深度学习调度程序， Pollux将平均作业完成时间减少了37-50% ，并为每个作业提供了理想的资源和训练配置。 Pollux基于对有用作业完成进度提出更有意义的衡量指标，来提升深度学习作业竞争资源的公平性，并揭示了在云环境下降低深度学习成本具有新机会。

文章图片
Pollux的协同自适应调度架构。
论文三：DistAI:Data-DrivenAutomatedInvariantLearningforDistributedProtocols

文章图片
论文地址：https://www.usenix.org/system/files/osdi21-yao.pdf
论文摘要：分布式系统很难正确实现，主要原因在于其不确定性。找到分布式协议的归纳不变式是验证分布式系统正确性的关键步骤，但即使是简单的分布式协议也需要花费很长的时间。该研究提出了DistAI ，一个用于学习分布式协议归纳不变式的数据驱动自动化系统。 DistAI通过模拟不同实例大小的分布式协议并将状态记录为样本来生成数据。观察发现，不变式在实践中通常是比较简洁的， DistAI从小型不变式开始，并列举适用于所有样本的最强可能不变式。然后， DistAI将这些不变式和所需的安全属性提供给SMT求解器，以检查不变量和安全属性的结合是否归纳。
从较小的不变式和可能的最强不变式开始，可以避免大型SMT查询，提高SMT求解器的性能。因为DistAI是从可能的最强不变式开始，如果SMT求解失败， DistAI也不需要丢弃失败的不变式，会单调弱化这些不变式，并用求解器再次尝试，重复该过程直到最终成功。
该研究表明DistAI能够找到「?-free」归纳不变式，如果存在该不变式，则能证明在有限时间内存在所期望的安全属性。该研究的评估实验表明， DistAI成功地自动验证了13种常见的分布式协议，并在验证的协议数量和速度方面都优于其他常用方法，在某些情况下，它的速度超过其他方法两个数量级。
下图为DistAI的工作流程，从IVy的分布式协议规范开始，首先， DistAI进行两阶段采样；其次， DistAI进行枚举操作；然后， DistAI将候选不变式提供给IVy ， IVy要么成功地将不变式与所需的安全属性结合作为归纳不变式，要么失败并指出不成立的不变式；最后， DistAI执行单调优化。

文章图片