使用形式化方法搜索traffic pattern空间，以queuing modules的形式对网络组件建模，并获得满足查询条件的工作负载描述。
网络模拟和仿真只能覆盖不断发展的网络工作负载的一个子集，为未被发现的角落情况和错误留下了空间，这些错误可能导致实时流量的次优性能。 来自排队论和网络calculus的技术可以为性能指标提供严格的界限，但通常要求网络组件的行为和流量的到达模式用简明和良好的数学函数进行近似。 因此，它们不能立即适用于新兴的工作负载以及为处理这些负载而开发的新算法和协议。
本文探讨了另一种方法：使用形式化方法来分析网络性能。 也就是说，用逻辑公式来模拟数据包，数据包在穿越网络时如何被每一块网络功能所处理，以及吞吐量和延迟等性能指标如何随时间变化。 然后，使用形式化方法界的验证和综合技术，可以详尽地探索所有可能的流量模式的空间，并找到那些网络无法提供令人满意的性能的模式。
两个独特的挑战
- 性能指标是刘级别的，并受到来自竞争性流量的数据包进入和退出网络组件的顺序和时间的影响。因此，对性能的推理需要对可能的packet-level
interactions的巨大空间进行推理。
- 文章找到了有效的方法来编码那些能够显著影响性能的交互过程
- 与其找到一个反例，更需要一种新类型的反例：一种traffic
pattern或者workload，它可以简明地捕捉到一整套可能经历不良性能的数据包跟踪之间的共同点。
- 使用syntax-guided synthesis。也就是说，先定义了一种用于指定工作负载的语言。然后，系统地搜索所有工作负载的空间，以找到一个使它所代表的所有数据包轨迹的性能差的工作负载。
Overview and Motivation
一开始先举了一个例子，说明FQ-CoDel作为Linux的default queuing discipline，存在一些bug，导致特定发送速率的流可能会引发性能问题。
Using Synthesis to Analyze Performance
主要分成以下几步
- Modeling contention points
- 用户以queuing modules的形式指定他们感兴趣的网络组件，每个组件有n个输入队列、一个处理模块、m个输出队列。
- 在验证引擎中，通过生成SMT公式，对这些队列和它们在连续T个时间步骤中的内容进行建模。
- 每一个时间步骤，每个输入队列都会收到数量有限的数据包。
- 此外，处理模块根据调度器的排队逻辑选择一个输入队列，从其中dequeue一个数据包，并将该数据包放入调度器的输出队列。
- Performance queries
- 接下来，用户查询他们感兴趣的一个性能指标，比如吞吐、延迟或者公平性。
- Introducing workloads
- 接下来，verification engine呢通过使用像Z3这种SMT solver来找到一个input packet trace，这个trace能够满足用户的查询。这里的packet trace就是一个assignment to the variables，表示每个time step有多少packets入队。
- 但上面的输出并不够好，因为它规定了每一个数据包进入的顺序和时间，而不是一些更加通用的场景。
- 论文中的工作负载定义为约束条件的组合，每个约束条件都规定了一个或一个子集的队列在一段时间内的流量模式。
- Synthesizing workloads
- 搜索引擎负责生成一个满足查询的工作负载。
- 它首先使用验证引擎来生成一组可以指导搜索找到合适的工作负载的例子轨迹。
- 接下来，它开始一个基于马尔科夫链蒙特卡洛（MCMC）的随机搜索过程，合成一个候选工作负载，并要求验证引擎验证该工作负载中的所有痕迹是否满足查询。
- 如果不满足，违规的痕迹将被返回给搜索引擎，并添加到示例痕迹中，以帮助指导寻找下一个候选工作负载。
- 这个过程不断重复，直到找到答案并返回给用户，用户可以终止分析或要求提供满足查询的其他工作负载。
后面主要是四大部分，不详细看了。