从生锈到火花：正式证明BIP缓冲区

我遵循嵌入式生锈群落的演变，特别是詹姆斯门斯的工作。基于BipBuffers，引起了引起我注意的项目是BBQueue，单一的生产者，单一消费者，锁定，线程安全队列。

此库的主要用法是异步处理数据进入或超出外设的数据，特别是在使用直接内存访问（DMA）时。

当从外围设备接收数据时，说明以太网控制器时，用户必须提供一块存储器，其中可以在接收时存储分组。一旦数据包完全接收，通常会有一个中断信号，以发信号到达分组的到达，并且必须非常快速地提供另一块存储器，以便在第一分组到达第一个数据包期间到达。大多数时间将在不同的上下文中处理数据和数据的处理，例如中断处理程序和线程。该分组必须通过各种协议进行解码，并且在结束时，必须向用户呈现数据。为了性能，复制潜在的大量数据块，因为它必须最大限度地减少用户。

缓冲区提供的区域的事实是封闭的是目的的核心。这对DMA使用至关重要，但更典型的循环界限缓冲区无法保证。此外，这是

詹姆斯的BBQueue使用原子操作来提供锁定缓冲区的无锁实现。这意味着生产者和消费者可以在不同的执行线程（或中断）中运行，并安全地使用BBQueue，而无需诉诸于ADA世界中的同步原语，例如互斥锁或受保护的对象。

我建议看看James Munns'博客文章以了解有关该算法和他的实现的更多信息，这篇文章的其余部分将更容易理解如果您这样做。请注意，自詹姆斯博客文章的出版以来，我用作该项目的基础的生锈实现，在实施中需要一些轻微的差异。

正如我试图上面的那样，BIP缓冲区对于嵌入式系统来说非常有用，甚至更为锁定实现。所以我开始一个项目将此解决方案带到ADA生态系统。但我想从生锈到ADA中的一个不仅仅是翻译，因此利用这个机会在混合中带来动画正式验证。

BBQueue实现主要在缓冲区中处理索引。有一个索引可以跟踪要写入的下一个内存，另一个用于读取的内存，等（参见James'Blog Post）。

使用Spark我想证明一些功能属性，将表明实施是正确的。例如，我想证明当授予可写的缓冲区时：

切片有效：下限和上限位于缓冲区的范围内

切片可写：下限和上限位于缓冲区的可写部分内

切片的大小等于所请求的大小，或者如果没有足够的可用空间可用

为了能够证明这些属性，我写了帮助函数来改进问题。下的功能表达了索引在可写区内的索引意味着什么：

函数in_wrable_area（这个：缓冲区; offset：buffer_offset）返回布尔值（如果是is_inverted（这）那么 - 已经反转 - | --- --- W ========== r ---- | - 倒（r> w）： - 我们可以在w .. r - 1偏移在这个..write ..这.read - 1 else（ - | ==== r -------- -w ===== | - 未反转（r <= w）： - 我们可以在w .. size - 1，或0 .. r - 1如果我们反转（offset .write。 。这个。这个.size - 1）或者（偏移在0 ..read-1））））;

从此功能易于编写有效可写切片的定义，然后将此定义用作授予可写切片的子程序的后期位置。

函数viply_write_slice（：beaffer; slice_rec）返回booleanis（valid_slice（this，slice），然后in_wrable_area（这，slice.from），然后in_wrable_area（这，slice.to））;程序授权（如下：在out buffer ; g：出于write_grant;尺寸：计数）与post =＆gt; （如果size = 0那么状态（g）=空），然后（如果状态（g）=有效，则write_grant_in_progress（此），然后切片（g）.length = size，然后是valid_slice（此，slice（g））和然后有效_write_slice（此，slice（g）））; - 请求连续可写切片的索引完全大小的元素

实现证据的另一个重要部分是缓冲类型上不变量的定义。在某种程度上，我认为这是解释火花自动普通的算法。

最后，我设法在代码上获得100％的证明。我还使用GitHub动作工作流程在拉出请求时自动运行GNATProve。如果你试图打破代码（https：// github .com / f a b i e n - c h o u / b b q u e y e-s p a r k / p ull / 2）您应该看到这样的消息：

Alire Package Manager Alire.ada.dev，提供了BBQueue的ADA / Spark实施。要将其导入项目，您只需运行此命令：

BBQueue Crate的根包实现仅处理索引的类型，而不具有内部缓冲区。这在多种情况下很有用。

1）在多个缓冲器中使用相同的切片。例如，在音频应用程序中，立体声左右频道可以在单独的缓冲区中：

声明左：sample_array（1。64）：=（其他=＆gt; 0）;右：sample_array（左边）：=（其他=＆gt; 0）;问：Aliased Offsets_Only（左＆＃39;长度）; wg：write_grant：= bbqueue.empty; s：slice_rec;开始授权（q，wg，8）;如果状态（WG）=有效，则S：=切片（WG）;左（左＆＃39; first + s.from ..左＆＃39; first + s.to）：=（其他=＆gt; 42）;对（右和＃39; First + S.from ..右＆＃39; First + S.to）：=（其他=＆gt; -42）;提交（Q，WG）;万一;

声明类型my_data是记录a，b，c：整数;结束记录;键入my_data_array是my_data的数组（自然范围＆lt;）; buf：my_data_array（1。64）;问：Aliased Offsets_Only（Buf＆＃39;长度）; wg：write_grant：= bbqueue.empty; s：slice_rec;开始授权（q，wg，8）;如果状态（WG）=有效，则S：=切片（WG）; Buf（Buf＆＃39; first + s.from .. buf＆＃39; first + s.to）：=（其他=＆gt;（1,2,3））;提交（Q，WG）;万一;

包BBQueue.Buffers仅基于偏移量_仅提供内部缓冲区。如果您只想分配内存块，这是一个更方便的包：

声明Q：别名缓冲区（64）; wg：write_grant：=空; s：slice_rec;开始授权（q，wg，8）;如果状态（wg）=有效，则声明b：storage_array（1 .. slice（wg）.length）与地址=＆gt;切片（WG）.addr;开始B：=（其他=＆gt; 42）;结尾;提交（Q，WG）;万一;

BBQueue的最后一个变体是Framed_ Buffer。到目前为止呈现的BBQueue实现，当消费者请求数据时，返回最大可读切片。然而，FRAMED_ BUFFER不断跟踪从生产者的每个提交的长度，并且返回给消费者的切片对应于提交。这对于具有可变长度分组的协议非常有用。

声明问：Aliased Framed_Buffer（64）; wg：write_grant：=空; RG：Read_Grant：=空; s：slice_rec;开始授权（q，wg，8）; - 获得8项提交（Q，WG，4）; - 仅提交4拨款（Q，WG，8）; - 获得8个提交（Q，WG，5）; - 仅提交5读（W，RG）; - 返回大小的授予4

据称在这篇文章的开始时，BBQueue是一个锁定的线程安全实现的BIP缓冲区。为了实现实现的锁定属性，原子序操作用于读取，写和修改索引。

为此，我创建了另一个驻地箱，提供了通过内在原子函数的火花绑定。

合同被添加到绑定子程序规范中，以允许Spark Provers了解原子内涵所做的内容。例如：

通用类型t是mod＆lt ;; package atomic.gener8with预先制定，spark_modeis类型实例是有限的; - 此类型是有限的，私密，只能使用下面的 - 原语来操纵。过程add_fetch（：alized实例; val：t;结果：out t; sourd：mem_order：= seq_cst）与post =＆gt;结果=（值（此）＆＃39;旧+ val），然后值（此）=结果;

这个项目是我的第一个Spark项目，并获得100％的自动证明是一个具有挑战性的任务。现在已经完成了，维护代码的成本大大降低，这项初步努力将长期支付。

一如既往，欢迎反馈，如果您发现对项目有用的此实现，请随时告诉我们。

在Epita（巴黎）的工程学位之后，Fabien于2010年加入了adacore。他参与了实时，嵌入式和硬件仿真技术。他的业余时间制造商/ DIYER包括电子，音乐和木工。