FLash-1

Flash-解决更新风暴、长尾到达的最新数据平面验证-学习2

一种声明性需求规范语言

<packet_space, sources, path_set>的含义
所有数据包来自packet_space，都可以从sources中设备进入网络，并必须沿着属于指定为正则表达式的path_set的至少一个路径转发

示例
<sip = 10.0.1.0/24 and dip = 10.0.2.0/24,[S],S.W.*＞$>的含义
对于在设备S处进入网络的源IP在10.0.0.0/24中且目标IP在10.0.2.0/24中的任何数据包，能够到达至少一个具有可到达数据包目的地的外部端口的设备，同时指向设备W

IMT的形式化理论

基本概念

计算有效断言

假设第1个设备只有两条规则p1和p2 
p1=(dstip=10.0.0.0/24 pri=2 forward port1)
p2=(dstip=10.0.0.0/16 pri=1 forward port2)
显然 p1的优先级更高 因此p1的有效断言=transfor(10.0.0.0/24)
但是p2的有效断言显然不是 p2的优先断言=transfor(p1∩(否定)p2)
即p2的实际部分应该是10.0.1.0——10.0.255.255 即不包含p1 可以使用下面公式表示

如何进行模型转换R(基于规则的)->M(基于等价类的)，公式如下
公式的含义就是所有规则的有效断言的union 通过这个公式就完成断言的转换

规则更新（插入或删除）

规则更新无非有两种：插入规则与删除规则
插入规则：设备原始规则（优先级比新规则低）有效断言减少
删除规则：设备原始规则（优先级比新规则低）有效断言增加

规则逐条更新效率很低

原因：假设存在两条规则集r1，r2，规则集中分别包含2，3条
r1规则集：
r11=(dstip=10.0.0.0/24 pri=2 forward port1)
r12=(dstip=10.1.0.0/24 pri=2 forward port1)
r2规则集：
r21=(dstip=10.0.0.0/16 pri=1 forward port2)
r22=(dstip=10.1.0.0/16 pri=1 forward port2)
r22=(dstip=10.2.0.0/16 pri=1 forward port2)
首先计算r1的有效断言
eff_r1 = eff_r11 ∪ eff_r12
再计算r2的有效断言
eff_r2 = (eff_r21 ∪ eff_r22 ∪ eff_r23) ∩ (否定)(eff_r11 ∪ eff_r12)
我们可以注意到 eff_r11 ∪ eff_r12 已经在计算eff_r1时计算过了，如果单独更新规则集r2，则会产生冗余

问：作者是如何解决这个问题的？
答：检查两个断言是否可以合并，若插入的断言p1和断言p2有相同的动作(转发到port1)，则可以创建新的断言
p=p1∪p2，这样再计算有效断言时可以减小冗余，缩短时间

input:数据包头部
output:转发行为
注意：IMT不处理具体某个input，而是处理input集合

覆盖允许更新组合的运算符

新的更新（S3-S2-S1）到来后，首先发生在设备S3，即下图中ΔR3
由于存在两条规则，因此有两次更新
更新1：ΔR3中第一行，重写运算符就是(Δp=p4,Δy)，其中Δy指定了采取的动作，从S3到S2，写作y3=S2；
然后将该断言与原本断言就行交集运算，判断，有以下两种情况：
<1>为空，该重写运算符不起作用
<2>不为空，相交的部分成为新的等价类，其余部分不变（类似于APKeep中分离断言）
更新2：ΔR3中第二行，重写运算符就是(Δp=p5,Δy)

reduce1:键是Δy，对于具有相同键(Δy)的断言，断言(Δp)被减少
reduce2:键是Δp，对于具有相同键(Δp)的断言，断言(Δy)被减少
这两步都能提高效率

如下图所示
在S3处reduce1 就是将p4与p5合并，即p3=p4∨p5
reduce2 就是将ΔM1、ΔM2、ΔM3进行Δy合并，即Δy={y3=S2,y2=S1,y1=A},即{A,S1,S2}

注意：map-reduce过程仅适用于无冲突覆盖。
冲突覆盖的概念：
两个覆盖运算符(Δp,Δy)和(Δp′,Δy′)存在冲突，当且仅当Δp和Δp′相交，并且它们在同一设备上写入不同的动作。

应用

高效计算ΔM

以下算法是规则更新后，根据ΔR计算ΔM的算法
输入：ΔRi:第i个设备的本地更新块 Ri:更新前已排序的初始规则
输出：ΔMi:等价于ΔRi的原子重写集合 Ri':更新后已排序的最终规则
步骤
L1:移除ΔRi中无用的更新 （先增加后删除 或 先删除后增加）
L2:排序ΔRi按优先级降序排列
L3:Rdiff为MergeBlockAndDiff(Ri,ΔRi)的结果
L4:Ri'=Ri 将更新赋值于Ri'
L5:ΔMi为CalculateAtomicOverwrite(Ri',Rdiff)的结果
L6:返回Ri'，ΔMi
具体函数含义
函数：MergeBlockAndDiff(Ri,ΔRi) 合并本地更新
    L8-L11:初始化
L8:Rdiff初始化为空列表
L9:优先级较高的规则是否被删除higher初始化为false
L10:r初始化为Ri的最高优先级
L11:δ=(op,rδ)是ΔRi中最高优先级的更新
    L12-L16:首先定位应该应用更新的位置。
L12:首先判断δ是否为空，不为空（表示存在更新）
L13:判断ΔRi中最高优先级的规则rδ是在r之后增加/删除的，如果是
L14:判断优先级较高的规则是否被删除higher是否为true，如果是
L15:扩展Rdiff，即Rdiff.add(r)
L16:遍历Ri的下一条规则，并赋值于r
    L17-L20:插入更新
L17:如果ΔRi中最高优先级的规则rδ不是在r之后增加/删除的
L18:如果最高优先级的动作是插入
L19:在规则r前增加rδ
L20:扩展Rdiff，即Rdiff.add(r)
    L21-L24:删除更新
L21:如果最高优先级的动作是删除
L22:从Ri中删除r
L23:优先级较高的规则是否被删除higher为true
L24:遍历Ri的下一条规则，并赋值于r
L25:获取ΔRi中下一个更新δ
L26:若δ为空，判断优先级较高的规则是否被删除higher是否为true，如果是
L27:将Ri中剩余规则添加到Rdiff
L28:返回Rdiff

该算法主要是计算ΔM 即reduce1，该算法并没有实现断言的合并

快速IMT

输入空间分区:快速IMT的复杂性取决于反向模型和更新的大小，这两者都与数据平面中的规则数量有关。通过将空间划分为多个子空间，可以减少更新过程中有效对的数量，以及受影响规则的数量。因此，它可以大大提高模型更新的速度。
快速查找重叠规则:计算原子重写(ΔMi)是计算每个受影响规则的有效断言。可以看出，规则的有效断言r将影响或受其他规则影响r'，只有当它们的匹配重叠时。mr∧mr'≠∅. 在一些常见的场景中，例如，当数据平面主要由最长前缀匹配规则组成时，重叠规则的数量通常远小于设备上的规则数量。为了加快原子覆盖的计算，Flash使用多维前缀Trie[24]来实现对重叠规则的快速查找。
PAT:

早期检查

目前数据平面验证工具存在的问题

问题

<1>如何调度规则更新来构建与收敛状态一致的模型？

<2>如何在信息不完整的情况下有效地计算验证结果？

Flash是如何做的

<1>识别一致的FIB更新，即从相同的网络状态计算的更新

<2>识别潜在的收敛状态

<3>将潜在收敛状态（为了效率）的一致FIB更新（为了正确性）调度到同一验证器

识别与Epoch一致的FIB更新

Flash使用网络状态来表示路由软件用来计算转发规则（例如，链路状态和前缀配置）的信息。
随着网络的发展，其状态也会因不同事件（如链路故障）而发生变化。在同步状态协议中，状态更改会传播到整个网络。

Flash通过将不同网络状态计算的规则更新划分为epochs来区分这些更新。
具体来说，每个epoch表示全局网络状态的快照。
由于仅通过查看数据平面无法确定更新是否来自同一网络状态，Flash使用代理增强了路由软件。
代理计算标签(OpenR实现中，Flash使用密钥的哈希值和状态变量的版本作为epoch标签)，即epoch的唯一标识符，并将标签与根据状态计算的FIB更新相关联。
Flash要求代理和调度器之间的消息传递是串行的，即，来自同一设备的更新总是以与生成更新相同的顺序接收。
然而，Flash对来自不同设备上的代理的消息没有任何限制。

通过Epoch依赖性跟踪识别潜在的聚合状态。
由于Flash需要设备和调度器之间的严格顺序，如果调度器在接收到具有t2的更新之前在设备i上接收到具有t1的更新，则t1不能是收敛状态。
类似地，如果我们在t3之前看到t2，即使t2是设备i上的最新标签，我们也可以推断t2不可能是收敛状态。这被称为分布式系统中的“先发生后发生”关系，表示为t1≺t2。
Flash维护每个设备的最新标签和一组没有后续epoch的“活动”epoch。
一旦从设备i接收到新标签tnew（其旧标签为ti＝told），Flash就从活动集中删除told，并用tnew替换tell。
如果tnew没有被标记为非活动（由另一个设备），Flash会将tnew添加到活动集。标记在活动集中的epoch是一个潜在的收敛状态。

调度一致的FIB更新
由于更新与epoch标签相关联，Flash维护了从epoch标签到验证器的映射。
具体地，在从设备接收到具有新epoch标记t的更新时，
Flash首先将更新附加到设备的更新队列，并检查t是否在活动集中。
如果t不在活动集中，这意味着同一设备将来会有更新，则不需要进一步操作。
否则，如果t在活动集中，Flash会找到（或创建一个，如果不存在）t的验证器，并将更新从设备的更新队列馈送到该验证器。
在实践中，Flash可能需要采用退避机制，以避免由于控制平面错误或对不稳定链路的不当处理而快速创建验证器。

一个示例更新设置如图3所示。考虑由两个链路故障触发的更新:(S,W)和(B,Y)。
假设每个设备的初始标签为t0＝[0，0，…]，其中第一个/第二个元素是链路(S,W)/(B,Y)的描述。
假设在时间T1，Flash接收来自具有标签t1＝[1，0，…]的S的更新（在看到(S,W)的故障之后），以及来自具有标签t2＝[0，1，…]（在发现(B,Y)的故障后）的交换机A和B的更新。
在T1，t1和t2是潜在的收敛状态，并且被置于不同的验证器中。
然而，如果在时间T2>T1时，Flash从交换机S、A和B接收到更新，并且epoch标记t3=[1、1、…]，则调度程序将把T1和T2标记为非活动，并为t3创建一个新的验证器，因为t3现在处于活动状态。
然后，如果Flash从交换机E接收到标记为t2的更新，则Flash只需将更新附加到E的队列中，而不将其发送给任何验证器。
当它从E接收到具有t3的更新时，它将更新刷新到与标签t3相关联的验证器。
图4（a）显示了为每个epoch构建的模型，并在底部显示了不一致状态的示例。

通用正则表达式需求的一致性早期检查

作者首先指定了Flash如何对正则表达式中指定的一般要求执行一致的早期检测

图16给出了Flash中需求规范语言的简化语法

验证图和一致部分验证
Flash计算验证图，作为网络自动机和需求表达自动机的叉积自动机Gp，用于每个数据包空间H和一组源src。
初始验证图包含G中的所有路径，这些路径
（1）从srcs开始
（2）匹配所有正则表达式
考虑图3中的网络和需求。要求是子空间中的数据包ℎ在S处进入的数据包必须沿着穿过W和Y之一的简单路径到达D。
图4(b)显示了初始状态S1和接受状态D1的验证图。
有了这个图，对需求表达式的验证就相当于在验证图中找到一条可以达到接受状态的路径。
具体地说，如果存在这样一个仅由同步节点组成的路径，则该需求始终得到满足。
如果存在一条仅由同步节点组成的路径，则拒绝状态将始终不满足要求。否则，验证结果未知。

递减更新和可达性查询。
随着越来越多的节点变得同步，该epoch网络中可能符合需求的路径集正在单调减少。
考虑图3中的示例，在接收到图4（b）中的Update1之后，验证图只包含绿色区域中的节点和边。
在进一步接收更新2之后，Gp中没有有效的路径，这意味着无论如何，都无法满足图3中的要求ℎ 由其他设备转发。
在这种递减图中的可达性查询（即，边总是被移除，但从不添加）具有恒定的时间复杂性[41]。该算法的细节和伪代码，以及如何将其扩展为对更复杂的流量模式（例如，任意播、多播和覆盖要求[27]）执行早期检测，见附录D.2。

一致早期循环检测技术

简单来讲有两种方式
1.删除非同步节点，判断同步节点间是否存在循环 -> 缺点：容易错过早期检测机会
2.保持非同步节点，假设非同步节点的所有下一跳是任意一个接口，系统枚举所有可能，计算是否存在循环 -> 缺点：计算代价高

Flash结合这两种方法 提出hyper node compression方法
hyper node compression：
未同步节点的每个连接组件都被压缩为超节点，以降低枚举成本。
设U表示非同步节点的连通分量，该连通分量由超节点w代替。对于每个(u,v)∈E，u∉U和v∈U，移除(u,v)并向E添加边(u,w)。
用超节点验证此图将给出与第二种方法相同的结果，但避免枚举U中的路径。

请考虑图5中的示例。在图5(a)中，当sync={A,B}时，我们可以将未同步的节点C和X合并为一个超节点，表示为C&X。
在这种情况下，
可能存在一个循环，例如B→A→C&X→B，是原始图中B→A→X→B，
或者是无循环，例如B→A→C&X→out，是原始图中是B→A→X→C→out，
因此最终结果尚未确定。
然而，如果C是同步的，如图5(b)所示，Flash报告说，只要X不丢弃数据包，就会在最终状态下出现循环。如果只验证同步节点，则无法检测到这一点。

增量检测
Flash不检测来自所有可能节点的循环，而是只检测包含刚刚同步的节点的循环。
设VS和V'S相应地表示同步节点的旧集合和新集合。
如果在旧图中未检测到循环，则新图中的新循环必须包含V'S\VS中的节点。
结合超节点压缩(hyper node compression)和增量检测，Flash增量检查新的同步节点。

定义1：(input space,predicate,selection)

L:表示input的位数
input space:所有可能input值的集合 X={0,1}^L
predicate:布尔函数p:X->{0,1}
selection:{x∈X|p(x)=1}
P:X上的断言空间 
p0：对于x∈X，都能表示满足p0(x)=0的断言

赏

×

纯属好玩

扫码打赏，你说多少就多少

打开支付宝扫一扫，即可进行扫码打赏哦