嵌入式软件设计中动态数据结构的形式化描述

理论计算机科学电子笔记108（2004）99-112www.elsevier.com/locate/entcs嵌入式软件设计中形式化描述动态数据结构的初步研究埃德加·G日光a，b，1Bart Demoenb，2 Francky Catthoora，c，1a比利时Heverlee，Kapeldreef 75，B-3001，IMEC vzw，b鲁汶天主教大学计算机科学系Celestijnenlaan 200 A，B-3001 Heverlee，比利时c电气工程系，Katholieke Universiteit Leuven，Kasteelpark Arenberg10，B-3001 Heverlee，比利时摘要在嵌入式多媒体社区中，设计人员在不同的抽象层次上处理数据管理，从抽象数据类型和动态内存管理到物理数据组织。为了实现能耗、内存占用和/或执行时间的大幅减少，必须进行数据结构相关的优化。 然而，描述和实现这种优化的实现方式的复杂性是巨大的。因此，存在强烈的实际需要来明确地（即，数学地）描述这些复杂的动态数据组织。本文的目标是正式描述我们在以前的应用程序相关工作中实现的数据结构和访问操作（简称动态数据结构）。 我们通过（a）扩展分离逻辑的语法和语义-最近在程序验证社区中开发的逻辑-以及（b）将其用作我们应用程序的特定语言来实现这一点。这项工作的短期好处是，它允许嵌入式软件设计人员明确地表达，从而更容易地探索低成本的动态数据结构。 在实践中，这意味着设计者可以清楚地推理，从而实现非平凡但最佳的动态数据结构。从长远来看，它的好处是为未来的优化编译器提供了一条途径，以增加与动态数据管理相关的全局优化范围。保留字： 嵌入式系统设计，分离逻辑，动态数据结构1 电子邮件：{voudheus，catthoor}@imec.be2 电子邮件：{bmd}@cs.kuleuven.ac.be1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.01.015100例如Daylight et al.理论计算机科学电子笔记108（2004）991介绍在嵌入式平台上设计和实现低成本的数据结构实现是一项繁琐的（即耗时且容易出错）任务。但在嵌入式多媒体应用的背景下，这项任务是极端重要的。由于数据在这个应用领域中占主导地位，如果在设计轨迹的早期就考虑到应用程序的数据结构，就可以产生非常高效的代码。这意味着不仅需要验证实现（即设计轨迹的输出）。此外，系统地探索各种数据组织的能力[3，14]（同时遍历设计轨迹）对设计师有利。我们关注的正是后一个问题1.1低成本动态数据结构我们激励我们的正式工作，提出一个数据结构转换的例子。在图1（a）中，通过向数据结构1添加链接，将初始数据结构1转换为数据结构2。这些链接允许容易地遍历数据结构2，这通常导致平均数据访问量的减少。另一方面，由于额外的链接，内存占用增加了。在数据访问和内存占用之间存在明显的权衡。当数据集的大小增长时，这种权衡可以跨越很大的范围。r =数据记录数据结构1（一）= link数据结构2输入数据结构R1R7输出数据结构r1 r3R7（b）第（1）款Fig. 1. （a）在记录数组之上添加链接数组。(b)一个动态的例子：在数据结构1中插入一个记录。在上面的例子中使用的遍历操作是一种访问操作，其中需要查询数据结构中所有存储的记录（r）。 由于多媒体应用的动态行为，在数据结构中存储哪些记录并不是先验已知的。Traffic是多媒体应用程序中一个非常重要的访问操作，在[4]中的各种案例研究中已经证明了这一点。这意味着，由于数据访问次数的减少，存储器相关的能量消耗对于数据结构2（与数据结构1相比）可以急剧降低，即使存储器占用已经增加。头R1R7R1R7例如Daylight et al.理论计算机科学电子笔记108（2004）99101在我们以前的工作[4]中，我们已经探索了各种数据结构和相应的转换。我们在这里只提出了一个转换，但在实践中，我们应用各种转换顺序，从而获得低成本，但难以理解的数据结构和相应的访问操作。我们在探索过程中面临的问题是，如果不使用代码实现数据结构，就无法准确地说明数据结构2（或数据结构1）的含义。造成这一问题的因素有两个。(i)实现复杂的动态数据结构的过程是一个耗时且容易出错的过程。(ii)即使成功完成了实现阶段，其他设计者甚至同一设计者也难以从代码中提取和理解数据结构及其访问操作。在本文中，我们解决的确切问题是一个正式的模型，允许设计人员companimously和明确表达的确切行为的非平凡的，但成本低的动态数据结构的发展。我们的概念是分离逻辑[9，10，11]在语法和语义方面的扩展，并将其用作动态数据结构的规范语言在本节的其余部分，我们将展示我们在形式化方面的两个主要贡献：（i）稀疏性和（ii）访问操作。我们以数据结构1为例。我们可以互换使用数据结构和堆这两个术语。例如，数据结构1是堆1的同义词。稀疏性为了描述数据结构1的空间方向，我们可以在下面的规范中使用分离逻辑的*好吧 1. 第七章.（l <$→_）*（l +1<$→ r 1）*（l +2 <$→_）*···*（l +6 <$→_）*（l+7<$→ r 7）规范指出，数据结构包含从位置l开始的八个连续堆单元。数据结构的稀疏度为2（总共8个元素）。然而，这种规范过于严格，因为它精确地指定了哪两个堆单元包含一条记录（即r1和r7），而不是表示八个堆单元中的任何正是这种特性需要被建模，因为它是用于嵌入式多媒体应用的动态数据结构的复杂性的主要来源。稍后我们将展示如何正式处理稀疏性。访问操作另一个更基本的问题是无法在分离逻辑中对（数据结构的）变化建模。考虑例如在数据结构1中插入记录r3，如图1（b）所示指定堆更改（或102例如Daylight et al.理论计算机科学电子笔记108（2004）99数据结构的变化），我们需要扩展原始的语法和语义，以包含输入堆和输出堆的概念。输入堆对应于原始数据结构（即在插入发生之前）。输出堆对应于包含记录R3。插入只是我们在本文中正式定义的访问操作之一。1.2概述我们将在第2节介绍相关的工作，并在第3节重新介绍分离逻辑的所有相关的初始工作。我们在第4节中以两种不同的方式扩展了分离逻辑，以处理稀疏和访问操作。在本节中，我们对图1（a）的数据结构1进行建模。由于空间有限，我们参考了一份技术报告[5]，其中我们展示了我们的规范语言的所有语法和语义，并完全建模了图1（a）的数据结构2。我们在第5节中陈述了我们的结论。2相关工作除了引言中给出的参考文献，来自验证文献的其他灵感来源是[15，1]。杨[15]讨论了分离逻辑的可靠性和完备性。Ahmed等人[1]使用类型系统结合分离逻辑的变体来描述分层内存布局。程序验证社区和我们的（嵌入式系统）社区之间的区别在于，我们不开发用于验证命令式程序的逻辑。我们使用和扩展的语法和语义的原始逻辑，以模型的数据结构和访问操作。其目标是帮助嵌入式系统的设计者表达复杂但低成本的动态数据组织。可靠性、完整性和其他逻辑属性与我们（当前）的目标无关当设计和实现嵌入式（例如手持）设备时，降低给定任务的能耗是主要目标[2，3，6]。在多媒体子领域，嵌入式系统，数据管理是功耗的主要贡献者[3，6，12，13]。多面体模型[8，3]经常在这个社区中使用（例如，在优化工具中），以对数据存储和数据访问进行系统建模我们的规范语言在两个方面与嵌入式系统社区中当前使用的数据组织首先，我们描述了复合数据结构的子部分之间的相关性，而不是仅仅将复合数据结构建模为一组不相关的子部分。例如Daylight et al.理论计算机科学电子笔记108（2004）99103∈∈--{}∈∈ −{}相关数组例如，一起形成图1（a）的数据结构2的两个数组以特定的方式相关。 我们对此进行了明确的建模（见[5]）。其次，我们区分了应用于所研究的数据结构的不同类型的数据访问。例如，我们区分对应于插入记录的数据访问和对应于删除记录的数据访问，而不是简单地将两者建模为物理访问而没有进一步区分。这两个额外的信息来源明确考虑在我们的形式主义。如果正确利用，这些有价值的信息可以显着降低能耗，内存占用和/或执行速度（如我们以前的工作[4]所示）。3分离逻辑本节中的所有基本概念都来自我们重新介绍这些概念只是为了教学的目的。不熟悉分离逻辑的读者建议阅读[11]。3.1堆栈与堆为了描述数据组织，我们使用堆栈和堆。 元素S是堆栈，dom（s）表示堆栈s的域。 元素h H是堆，dom（h）表示堆h的域。堆栈将变量映射到值。堆将位置映射到值。值可以是整数，原子或位置。(1)V al=IntatomsLoc S=V ar~finV al H=Loc~finV alLoc =我... . 是一组位置和lLoc。 l +1 Loc和（l+1）1 =1。Var=x，y，.. .是一组变量。原子=零，a，. . 是原子的集合。我们使用~fin表示有限部分函数。3.2语法表达式E在表1中给出，其中E1和E2都是整数或位置。在后一种情况下，位置上的加法和减法仍然需要定义。分离逻辑是经典（谓词）逻辑的扩展。空堆、空间合取和空间蕴涵3构成了这个扩展。非原子式β在表1中给出，其中P和Q是非原子式。原子式α如表1所示，其中3本文中没有使用空间蕴涵。104例如Daylight et al.理论计算机科学电子笔记108（2004）99∩⊥∈∈⊆∈|∈- -∈∈表1语法E：：=X可变β：：=α原子公式|42整数|假虚假性|||无aL无原子位置|||PQempP *Q古典意蕴空堆空间连接||E1+ E2E1− E2此外减法||P→*QP.P.空间含义潜在量化|α：：=|···E1=E 2E1inM∈I→ H.v∈/dom（s）annd设m=[[E1]]s∈Int，i，j∈I。i=/Mi<$Mj，j表示n=[[E2]]s∈Int，I={i |m ≤ i ≤ n}这允许我们定义一个数组。h={Mi |i ∈ I}和i ∈ I. [s|v <$→ i]，Mi|= Pn1k=0这等于：（l_）*（l + l_）*. * （1 + n 1）。该阵列在图2（b）的顶部描绘，其中n= 8。注意，（2）的右边是一个公式。每当符号数组l n用于规范中，应替换为公式k=0n−1n（l+k<$→_）. 为了方便起见，我们有时将（2）称为For-我们可以声明数组的属性。 例如，lookup属性：(3)lookup l n indexval（0≤indexn）<$（l+index›→val）<表示（i）值索引位于由0和n定义的范围内，(ii)当前堆在位置l+index处包含值val。为了说明所调查的数据组织是具有查找属性的数组，我们断言：n.指数. Val. （array l n）（lookup l n indexval）.对于给定的堆栈s和堆h，如果存在l和n，使得对于位于0和n定义的范围之间的所有索引值，存在val，使得n−1（l+k<$→_）并且（l+index›→val）保持。即使公式（3）自然地从公式（2）得出，我们仍然明确地陈述公式（3）。回想一下，我们的目标是描述数据结构的特定属性，而不管这些属性是否可以从其他逻辑公式导出（参见第2节，我们将我们的工作与程序验证社区联系起来）。数组的另一个属性在公式（4）中给出，公式（4）是P108例如Daylight et al.理论计算机科学电子笔记108（2004）99∃ ∃ ∃ ∃∧v=E1Js，h|= Spars espSJk=0归纳定义4.它描述了如何遍历数组。遍历的边界由l和n定义，被查询的当前堆单元由i表征，函数f被应用于存储在当前堆单元中的值v，res是表示遍历期间所有函数应用的总和(4)遍历l n i fres（ emp（ res= 0））((0 ≤ i i，j ∈ J. i/= j意味着MiMj和h={Mj |j ∈ J}和j∈J. [s|v<$→j]， Mj|=P图2（b）的中间给出了稀疏性的一个具体例子，其中sp=2。数学公式为：sparse l nsp稀疏spn−1（l+k<$→_）它描述了数组的子堆。子堆由sp堆单元组成。[4]我们不分析这个归纳定义的终止性。对于本文中的其他定义，我们也不这样P例如Daylight et al.理论计算机科学电子笔记108（2004）99109G›→Jn−1sparselnspSparseActive（l+k<$→_）spJ−arrayln（l+k<$→_）||4.1.3空间减法从数组中减去稀疏数组会得到一个碎片数组（参见图2（b）中底部的数据结构）。我们表示如下。碎片化（array l n）g（sparse l n sp）g连接词，我们称之为空间减法，定义如下。s，h|=PgQih'。“啊”。 h=h"−h“和s，h"|=P和s，h'|=Q可以根据（3.2节的）原始语法来定义，但为了简洁起见，我们省略了这一点。4.1.4主动与被动记录由sparse l n sp描述的堆不等同于图1（a）中的数据结构1，因为该堆仅包含sp堆单元，而数据结构1包含所有n个堆单元。在数据结构1的情况下，总共sp个堆单元包含活动记录（即，r1和r7），所有其他堆单元包含被动记录 。 为 了 指 定 数 据 结 构 1 ， 我 们 引 入 了 一 个 新 的 表 示 法 ： Active （ E1E2）。 这个符号断言对应E2堆单元是活动记录。我们将以下更改应用于初始语义H=Loc~finV al× {Active，Passive}s，h|=E 1 <$→ E 2i <${[[E 1]]s}=dom（h） 和 h（[[E 1]]s）=[[E 2]]s，_s，h |= Active（E 1 <$→ E 2）i <${[[E 1]]s}=dom（h） 且h（[[E1]]s）=[[E 2]]s，活动使用Active允许我们精确定义一个稀疏数组：SParray l n sp。这是图1（a）的数据结构1。n1k=0k=0fragmentationl n sp（array l n）g（sparse l n sp）Sparray l n sp（sparse l n sp）*（fragmentation l n sp）相应的图示见图2（c）4.2数组：访问操作我们扩展了原始的语法（3.2节）和语义（3.3节）来模型改变。我们通过将关系式s，h=P改为s，hi，ho=P来实现这一点。我们使用hi表示输入堆（即发生变化之前的堆），ho表示输出堆（即发生变化之后的堆）。我们不将堆栈s拆分为输入堆栈si和输出堆栈so。我们提出了扩展的语法，额外的符号，和相应的se-mantics。基于这些扩展，我们指定了数据结构1的各种访问操作。110例如Daylight et al.理论计算机科学电子笔记108（2004）99.（hi，ho）。喜和表示海岛喜，何。ho喜和表示4.2.1语法附加的非原子式β是：β：：=empi空输入堆| empoEmpty Output Heap|相同IIOH| Same (R) IIOH and both model R| P ; Q顺序组合其中P和Q是非原子公式，R是仅描述一个堆的非原子公式。换句话说，R是3.2节的非原子式。IIOH是相同输入和输出堆的缩写附加的原子式α是：α：：=E1<$→iE 2 输入堆| E 1 ›→o E 2 Points to Relation in Output Heap我们使用empi表示输入堆h i为空，empo表示输出堆ho为空，而不是使用emp来表示（唯一的）堆h为空。我们用Same来描述hi和ho是相同的。类似地，当hi和ho都符合描述时，使用Same（R）R. 例如，s，hi，ho|=Same（（5›→3）* true）在语义上等价到s，hi，ho|=（（5 <$→i3）<$（5 <$→o3））* 相同。注意我们使用了两个不同的指向关系：<$→i表示输入堆hi，<$→o表示输出堆ho。顺序组合P;Q表示由两个连续堆更改组成的堆更改;即堆更改P之后是堆更改Q。4.2.2符号由于我们处理的是一个输入堆hi和一个输出堆ho，以便对堆的变化进行建模，因此我们扩展了堆的不相交性的概念（参见第3.3节）堆变化的不相交性。类似地，我们将不相交堆的并集的概念扩展到不相交堆变化的并集，这同样适用于集合包含。最后，我们定义了一对夫妇的预测，堆到一堆。我们用（hi，ho）。hJ，hj表示h ihJ 和HohJ. 同样地，.JJ我I.奥 吉吉OiJojhi±hJ 和ho±hJ。 Also，n1（h1，h2）=h1anddn2（h1，h2）=h2.4.2.3语义断言的语义由下式给出：s，hi，ho |= P，自由（P）自由度（s）. 类似地，（hi，ho）±例如Daylight et al.理论计算机科学电子笔记108（2004）99111```k=0“|我v=E1O我 OTHB表2语义s，hi，ho|=E1 = E2i[[E1]] s =[[E2]] ss，hi，ho |= P →sQi=h′，h′.如果“h'，h'“（hi，ho）s，hi，ho|=E1（l + index<$→o v））s Same（<$w. （l + index <$→i w）<$（l + index <$→o v））s相同的下标l n f<$v。（remove l n index v）;（insert l n index（fv））第3.1节的基本域保持不变。原始语法和扩展语法的语义子句在表2中定义。注意，在最后一个语义分句中，我们使用了3.3节中的关系s，h=R。除了表2的语义子句之外，我们还添加了迭代分隔连词的语义解释，但为了简洁起见，我们省略了（几乎相同的）稀疏ISC：s，hi，ho|=JE2P在<$M∈J→H× H中。我的v∈/dom（s）annd设m=[[E]]s∈Int，k，l∈J.k=/Mk<$Ml，我1l暗示1h=S{（Mk）|k∈J}和n=[[E2]]s∈Int，ho=S{\displaystyle\mathbb {2}（Mk）}|k∈J}an dJ={j |m ≤ j ≤ n}<继续阅读>J. [s |v <$→ k]，n1（Mk），102（Mk）|=P4.2.4访问操作在表3中，我们指定了一个数组，以及数组中记录的插入、删除和修改作为顺序复合的一个简单应用，我们将数组元素的修改指定为删除值v然后插入修改后的值（fv）的顺序复合。注意，对于在数组中插入记录，我们指定该值w被值v覆盖，而不管值w和v是否相等。112例如Daylight et al.理论计算机科学电子笔记108（2004）995结论在这篇文章中，我们已经解决了形式化描述动态数据结构的需要，因为它们发生在现实生活中，多媒体应用程序。我们已经建模的两个相关特征是（i）稀疏性和（ii）访问操作。在这样做的同时，我们以各种方式扩展了分离逻辑（一种在程序验证社区中使用的逻辑）的原始语法和语义，其中输入堆与输出堆的引入是最深刻的。作为我们的语法和语义扩展的应用，我们在本文中指定了图1（a）的数据结构1，在[5]中指定了数据结构2，无论是在空间方向还是在访问操作方面。确认第一作者感谢P. O'Hearn和C.卡尔卡尼奥帮他指定访问模式。引用[1] A.艾哈迈德湖Jia，L. Walker，[2] L.贝尼尼湾陈文辉，[3] F. Catthoor 等 人 ， “Custom Memory Management Methodology: Exploration of MemoryOrganisation for Embedded Multimedia System Design”[4] 例如，日光，D. Atienza等人， “Memory-Access-Aware Data Structure Transformations forEmbedded Software with Dynamic Data Accesses”http://www.imec.be/design/ddte[5] 例如，日光，B。Demoen，F. Catthoor，http://www.imec.be/design/ddte[6] D. Fisher，J. Lin，加州大学伯克利分校计算机科学部，伯克利，加利福尼亚州94720-1776[7] S. Ishtiaq，P.W. O’Hearn, “BI as an Assertion Language for Mutable Data Structures”, 2001年[8] W.凯利，W。李国忠，[9] P. O'Hearn，J. Reynolds，H.杨，“改变数据结构程序的局部推理”，中国科学院学报，2001年。 第1-19页，LNCS2142页，Sprin ger-Verlag。[10] D.J. Pym，例如Daylight et al.理论计算机科学电子笔记108（2004）99113[11] J.C. Reynolds，[12] D. Singh，J. Rabaey等人，“Power conscious CAD tools and methodologies: a perspective”570-594，1995年4月。[13] N. Vijaykrishnan，M. Kandemir等人，“Evaluating integrated hardware-software optimisationsusing a unified energy estimation framework”2003年。[14] S. Wuytack 等 人 ， “Transforming Set Data Types to Power Optimal Data Structures” ，Proc.IEEE Intnl.低功耗设计研讨会，加利福尼亚州拉古纳海滩，第51 -56页，1995年4月。[15] H. Yang，论文，UIUC，2001年7月