基于语义的程序资源使用定量分析方法的研究：半环上的静态分析在Java卡缓存行为中的应用

理论计算机科学电子笔记164（2006）153-167www.elsevier.com/locate/entcs半环上的定量静态分析：Java卡Pascal Sotin1 David Cachera2 Thomas Jensen3Irisa，campus deBeaulieu 35 042 Rennes，France电邮地址：{sotin,dcachera,jensen}@irisa.fr摘要我们提出了一个基于语义的技术建模和分析的资源使用行为的程序写在一个简单的面向对象的语言，如Java卡字节码。该方法基于Di Pierro和Wiklicky的定量抽象解释框架，其中程序表示为线性算子。我们特别考虑半环上的线性算子（如最大加），这些算子已被证明对分析离散事件系统的成本性质是有用的我们说明了我们的技术，通过Java卡的缓存行为分析。关键词：静态分析，资源使用，缓存行为，线性算子，半环1引言本文主要研究基于语义的程序资源使用的定量属性分析。存在许多用于估计资源使用的方法，从监视或模拟[8]执行到精确计算程序的复杂性，以及用于确定最坏情况执行时间的技术[6]。我们的方法是基于最近的一个框架，称为定量抽象解释，导致一个优雅的程序模型的基础上，线性算子向量空间，这是能够处理几种数量。定量语义模型，像他们的定性同行，通常是不可计算的，所以我们设计了一个抽象的技术来计算一个正确的近似感兴趣的属性。在定量的情况下，这通常是特定资源的程序消耗的上限1Irisa/CNRS/DGA2 Irisa/ENS Cachan（布列塔尼）3Irisa/CNRS1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.07.017154P. Sotin等人理论计算机科学电子笔记164（2006）153Di Pierro和Wiklicky [7]提出了一种概率语义的抽象解释，其中概率与转换有关。这自然会导致一个模型，其中程序被建模为由随机矩阵表示的线性算子。我们继续研究将程序表示为线性算子的想法，但我们感兴趣的是估计程序的资源消耗，在这种情况下，我们可以将任何数值量附加到过渡中，而不仅仅是0和1之间的概率-这迫使我们超越了随机矩阵。转换的成本可以模拟例如堆栈高度演变、对给定方法的调用次数，或者可以表示基准执行时间。在本文中，我们将重点讨论如何建模缓存未命中。我们依赖于一个标准的小步操作语义，表示为状态s之间的转换关系s→qsJ，sJ∈State，成本q∈Q与每个转换相关联。有一种直接的方法可以将这种基于规则的语义传递到矩阵表示，将成本与一对状态相关联我们开发了一种技术，抽象这种语义，以返回一个可计算的近似的整体程序成本。要做到这一点，我们利用的事实是，一个程序的语义可以表示为一个线性算子的Q状态，其中Q是域的考虑成本。我们为程序定义了两个成本的概念：从初始状态到最终状态的全局成本，它来自语义的传递闭包。当底层图中存在循环时，这个闭包就不存在了，但是我们能够给出程序的长期成本，这是循环中转换的平均成本。这个代价的计算依赖于关于幂等半环特征值的Perron-Frobenius定理的一个变体。本文件的结构如下。在第2节中，我们为Java Card字节码语言定义了一个定量语义，它显式地对Java Card程序的（非功能性）缓存行为进行建模。在第3节中，我们定义了相应的线性算子语义。对于一个给定的资源，我们建议，在第4节中，计算资源的全局消耗的程序执行从开始到结束。有时不可能计算这种全局成本，例如。 当程序是一个反应程序时，根据定义，它不会结束。在这种情况下，我们仍然给出长期执行的平均消耗。在第5节中，我们将讨论如何通过将该算子投影到更小的状态空间来近似程序的整体行为2数量语义学描述非功能属性的定量语义仍然使用包含执行的经典信息的状态，以便能够计算控制流程。它们还包含额外的信息，这些信息不会影响计算结果，但可能会影响我们处理的性质。计算机的高速缓冲存储器就是一个很好的例子，因为即使计算结果和控制流程在存在高速缓冲存储器的情况下不改变，执行时间也会被强烈修改。我们给出了Java Card语言的语义Java Card是Java的一个子集，专为嵌入在智能卡上的程序而在这种内存不足的情况P. Sotin等人理论计算机科学电子笔记164（2006）153155可用的和与客户的交互，关于存储器和时间的程序的提取信息是感兴趣的。JavaCard的底层机制JVM的非功能性行为通过诸如垃圾收集、线程和即时编译器之类的功能得到增强，这些功能使定量的非功能性属性的分析变得相比之下，Java Card机制更少，更简单，因此它是我们分析的更合适的2.1在JCVM中建模缓存行为Java Card语义中的状态是这样的：哪里• H代表对象堆;• f是帧栈（即过程调用栈）的帧标识符，fr是该帧栈的余数;• m是当前方法，ip是其中的指令指针。当前指令由函数Instrat（m，ip）给出;• L是一个包含框架局部变量的数组;• S是帧的操作数栈;• C是一组逻辑地址，表示在执行的这一点上哪些值在缓存中逻辑地址集的管理方式与缓存类似。例如，该集合的最大大小将适合物理缓存的大小，并且替换策略将模拟由缓存完成的替换策略（例如LRU，FIFO）。函数update对缓存行为进行建模：它将缓存的当前状态以及对程序或指令访问的逻辑地址的类型化访问列表逻辑地址可以有三种形式：• 堆。reference.short指定堆中引用为reference的对象的short索引的字段。• 本地. short指定局部变量，由帧的shortframeId。• 堆栈frameId.int指定帧frameId的操作数堆栈区域中的第n个整数元素。例如，如果t是操作数堆栈的当前大小，则t指定堆栈当前顶部的元素，而t+1指的是该顶部上一个字的元素对这些逻辑地址之一的访问可以是读τ（地址）或写τ（地址），这意味着类型τ的数据分别在该地址处被读或写。 类型信息对于计算数据项的大小和数量非常重要156P. Sotin等人理论计算机科学电子笔记164（2006）153可以同时放入缓存中可以使用基于数据大小的转换来表示数据，例如，writeτ（address[+1]）相当于writeτ（address+1sizeof（τ））。对于语义，我们不描述JCVM的201指令[4]，但我们依赖于通过中间语言Carmel[5]对JCVM指令的建模。这种语言具有更易于管理的指令数量下面，我们给出描述加载指令的规则作为示例。它对应于Java Card指令集，该指令集将类型化局部变量（索引为i）加载到操作数堆栈的顶部（例如，iload，aload）。InstAt（m，ip）=loadτi<$L[i]=d SJ=d：：S<$size（S）=tCJ=update（C，[readτ（local.f.i）;writeτ（stack.f.t[+1]）]）→q在示例中，q对负载转换的成本进行建模。它需要与所考虑的数量相一致。例如，如果我们对堆栈高度演变进行建模，则对于加载指令，q将为q=+sizeof（τ）。q的值从一个指令规则到另一个指令规则变化，并且可以是状态的函数。我们在下面给出我们所有语义规则的量的实例，处理nummbe r o f rabeadinggcachemi s s es.如果规则包含CJ=update（C，access），则Rmiss（C，access）设q=0否则函数nbRmiss（C，access）计算如果指令开始处的高速缓存是C，则由存储器访问列表access生成的读取高速缓存未命中的数量。此函数必须与更新函数一起实现，因为其结果取决于第一次访问之后的缓存策略。一个. nbRmiss的计算如下：nbRmiss c[]= 0⎧⎪101如果⎧a=读取mnbRmissc [a|r]= nbRmiss（update c a）r +⎪⎪m∈c0.00否则该算法处理第一次访问改变其余访问的数据存在或不存在的情况，但它可能非常昂贵。 为了实现效率，可以独立于更新函数对nbRmiss进行近似。这种近似依赖于高速缓存不卸载将在当前指令中使用的值的假设。⎪P. Sotin等人理论计算机科学电子笔记164（2006）153157Ji=1卢恩在负载转移规则的情况下，这两种算法具有相同的结果，即如果local.f.i∈C则为1，否则为0。这是一种特殊情况，因为唯一的读访问是访问列表的第一个，因此其他访问不能有侧面的效果。3线性算子语义Java Card的小步长、定量操作语义在State上引入了一个带标签的迁移系统，标签在Q中，迁移关系为→。State×Q×State，写作s→qsJ。这种转换表明从s到s的直接（一步）转换成本为q。这些酉转移可以组合成大步转移，使用两个算子，这将形成Q上的半环。成本本来可以用一种更一般的方式来定义，但这种可以说是相当有限的定义具有有趣的计算特性。Q上的算子定义了一系列转换的全局代价，s→q1... →qn sj=q1国家序列我... n.不洁. 这是写的，当x是(1) 运算符是结合的，并且有一个中性元素e。量e这是一个不需要任何成本的过渡。(2) 该操作产生了一个称为hr根的函数，其值为q或q1/n，s ucht hatnnq=q. 一个包含有n个transitions的等式，每个都包含n个q，将花费Q。如果代表×、+、max或，则x的n次方根将分别是x，1/x，x和x。当存在几种方法来从数据s，X={sxqxsJ}中获取数据状态J时，它们之间的全局成本使用运算符Q定义为q=x∈X q x. 这是写的Sq SJ。(3) 算子是结合的、交换的，是它的中性元。量“0”意味着不可能发生过渡。(4) 其中，X是X的分配元素，X是X的吸收元素。(5) q是幂等的，即q<$q=q，所以如果从a到b的几个转换具有相同的成本q，则全局成本也是q。定义3.1满足条件1、3和4的结构（Q，n，n）是半环。在条件5下，它被称为幂等半环。我们使用满足五个条件的结构，即幂等元半环具有一个n次方根运算，我们称之为代价半环。例如，（Time，max，+）是成本的半环，它导致了最坏情况执行时间的定义。当两个状态可以由几个花费不同时间的转换序列连接时，最坏的时间被占用。为了计算一系列转换的成本，我们将每个转换的成本相加。158P. Sotin等人理论计算机科学电子笔记164（2006）153使用适当半环的成本计算，很容易根据这个半环中矩阵的计算来定义。一步转换的集合可以等效地由矩阵表示，称为转换矩阵，定义为：M∈ MState×State（Q）s→qsJ惠Ms，sJ=q这里，MA×B（C）代表行在A中，列在B中，值在C中的矩阵集合。这个矩阵也可以看作是半模Q态上的线性算子;半模对于半环就像向量空间对于环一样。与跟踪语义的即使矩阵/线性算子的计算是优雅和充足的，我们给出了他们的等价计算，在一个更经典的跟踪语义。对于一个程序P，我们考虑它的初始状态、最终状态和它的迹语义，（P）tr：• 初始状态I是程序可以启动的状态• 最后状态F是机器停止执行的状态例如，在Java程序的main函数的返回⎧ ⎫<$q qs1∈I，<$• <$P）tr=s1→1. s n−1→n−1 s nsi→qisi+1，4计算全球和长期成本在本节中，我们用矩阵计算来表示给定程序的成本。可以计算两种成本• 如果程序终止，我们可以计算一个全局成本，它代表了程序从初始状态到最终状态的成本。• 对于非终止程序，我们可以计算长期运行成本，它表示转换周期上的平均成本。在下文中，我们使用成本半环（Q，n，n）。设M是表示程序P的定量语义的矩阵。M包含由操作语义的一个步骤引起的转换成本。Mk，其中矩阵的乘积取在所考虑的半环中，总结了长度为k的所有路径的转移成本。全局和平均成本是从这个想法开始定义的如果存在这样一个传递闭包M+，则它包含所有⎩P. Sotin等人理论计算机科学电子笔记164（2006）153159++将成本从任何状态转换到任何状态。∞M+=Mii=1如果与语义相关联的转换图包含循环或无限路径，则可能无法定义此传递闭包。在这种情况下，我们最好参考下面定义的平均成本定义4.1设I为程序的初始状态，即入口点和F是程序的退出状态P的全局成本定义为gc（P）={Mi，f |i ∈ I，f ∈ F}全局成本通过以下方式与标准跟踪语义相关：定理4.2f−1gc（P）={j=1QJ|σ1→q1。 . →qf−1σf∈P）tr，σf∈F}（1）证明f−1{j=1QJ|σ1→q1。 . →qf−1σf∈P）tr，σf∈F}f−1--j=1∞Q I|σ1→q1. →qfσ f∈（→. ）+，σ1∈I，σf∈F}n=（n=1{j=1QJ|σ1→q1。 . →qnσf∈（→. ）n，σ1∈I，σf∈F}）∞n=σ1∈Iσf∈F（（n=1{j=1QJ|σ1→q1。 . →qnσf∈（→. ）n}））我们以类似的形式推导出另一个定义：gc（P）= {M|σ1∈ I，σ f∈ F}=σ1∈Iσf∈Fσ1，σf+σ1，σf∞=σ1∈In=1σf ∈Fnσ1，σfMM160P. Sotin等人理论计算机科学电子笔记164（2006）153⊕n等式（1）在以下条件下被证明，这很容易通过n上的归纳法证明：na、b={j=1QJ|a→q1. . . →qnb∈（→. ）n}Q长期成本如果传递闭包M+不存在，我们将考虑矩阵的特征值在M不可约的情况下，这个值是唯一的，它由下式定义∞ρ（M）=（trMk）1/kk=1其中trM=nM. 这是由Perron-Frobenius定理（更多）得出的。1i，i确切地说，它的实例化为幂等半环，如[3]）中所发展的，其中指出不可约矩阵A的谱射线是A的本征值，并且相关的本征空间是由具有严格正分量的向量生成的一维向量空间。在矩阵是可约的情况下，我们可以将其划分为三角形矩阵的形式。有了这个矩阵，我们可以用类似的方法得到一个唯一的特征值。在程序P的所有最大迹都是有限的情况下，长期运行的概念没有意义。在这种情况下，上述公式产生一个特征值等于平均代价与迹语义的关系如下：ρ是P的迹中出现的所有圈的几何平均之和（下）。例如，如果我们在半环（Time，max，+）中工作，ρ（M）是每条指令所花费的时间的最大平均值，其中平均值是通过将该周期中花费的总时间除以该周期中的指令数5数量语义学表示程序的转移矩阵通常是无限维的，因此既不能在有限时间内计算传递闭包也不能计算特征值。为了克服这个问题，我们定义了一个抽象的矩阵-比具体的矩阵小，最好是有限的-可以用来近似计算与无限的原始矩阵。我们考虑了使近似正确的必要条件例如如果我们计算运行一个程序所需的最小内存，这个量的正确近似值必须大于有效最小值。抽象设M是幂等元半环（Q，n，n）上具体域C上的线性算子，对应于程序的转移系零MP. Sotin等人理论计算机科学电子笔记164（2006）153161nnn+1nn+1nn+1n+1半环的单位记为e，M∈ MC×C（Q）给定从具体状态C到一组抽象状态的抽象函数D，我们可以将此函数提升为线性抽象算子α：关于半环如下。⎧如果α（c）=d，则为αd，c=α否则，设M∈MD×D（Q）是抽象域D上的线性算子.抽象α的正确性条件是：α<$M≤DM <$α其中≤Q是由半环运算<$（q1≤Qq2惠q1<$q2=q2），≤D是它的矩阵扩张（N≤DPfi，j. Ni，j≤QPi，j）.正确性正确性条件意味着全局和长期成本的计算是正确的，即，是对混凝土成本的过度近似它来源于α、M和M的线性。定理5.1如果M+和（M）+存在，即在有限时间内收敛，则α<$M≤DM<$α<$α <$M+≤D（M）+<$α（2）如果ρ（M）和ρ（M）存在，即如果M和M不可约，则α<$M≤DM<$α<$ρ（M）≤Qρ（M）（3）我们证明（2），首先证明：<$n≥1，α<$M≤ DM<$α<$α <$Mn≤Q（M）n<$α（4）这是由n上的归纳法证明的。n= 1的情况是平凡的。然后我们假设α<$M≤DM<$α和α<$Mn≤D（M）n<$α。我们拥有：α<$Mn≤D（M）n <$α（α<$M）<$M≤D（（M）<$α）<$M（5）α<$M≤D（M）<$（α<$M）（6）αM≤D（M）（7）植物油α<$M≤D（M）<$α162P. Sotin等人理论计算机科学电子笔记164（2006）153d，dd，dd，d++（5）是正确的，因为和保持顺序≤Q，定义为a≤Qb惠ab=b，分别由于结合性和幂等性的，和分配性的把它翻过来。从（6）到（7）使用第一个假设。然后，我们对n求和（4），一为无穷大，两边各因子分解为ααα（M 1<$M 2）. ）≤D（（M）1<$（M）2<$.. . ）<$αα<$M ≤D（M）<$α我们现在证明（3）。设c和d满足α（c）=d。我们首先证明了Mc，c≤Qd，d。我们有α<$M≤DM<$α特别是（α<$M）d，c≤Q（M<$α）d，c改写成cJ∈C（αd，cJ<$McJ，c）≤QdJ∈D（Md，dJ αdJ，c）我们分解两个求和，这产生：cJ∈α−1（d）（αd，cJ McJ，c）cJ∈/α−1（d）（αd，cJ （c）≤Q（（MJ）<$αdJ，c）<$（（MJ）<$αdJ，c）dJ=α（c）dJ/=α（c）考虑到α的性质，它可以简化为：cJ∈α−1（d）McJ，ccJ∈/α−1（d）n ≤QMd，d证明到此结束。 由于幂等性，我们推断，对于任何d，c∈α−1（d）Mc，c≤QM通过对d求和，我们最终得到：MP. Sotin等人理论计算机科学电子笔记164（2006）153163c∈CMc，c≤Qd∈Dd，d164P. Sotin等人理论计算机科学电子笔记164（2006）153（男）类似地，由于对任何k≥1，我们有α<$Mk≤D（M）k<$α，我们证明：c∈Ckc，c≤Qd∈Dkd，dtrMk≤Qtr（M）k（tr（M）k）1/k≤Q（tr（M）k）1/k∞ ∞k=1（trMk）1/k≤Qk=1（tr（M）k）1/kρ（M）≤Qρ（M）Q这就完成了定理5.1的证明。给定一个基于M、M和α的正确抽象，我们可以根据M+和（M）+的存在性对其进行分类。M+存在M+不存在M+存在全球成本的过度近似∅（M）+不存在通过长期成本给出全局成本信息的近似法长期成本的过度近似5.1抽象的例子考虑以下JavaCard字节码中的程序片段：1：负载x2：istore t3：负载y4：iStore x5：负载t6：istore y七：……我们处理的数量是缓存中的最大读未命中数。管理整个状态和整个缓存通常会使精确计算的成本过高，因此我们将状态和缓存抽象为仅包含指令指针和最后访问的数据，并将抽象状态写为（ip，var），其中ip为指令指针和var是最后访问的数据的逻辑地址。我们使用半环（N {}，max，+）对读取未命中的最大数量建模。 如果n是缓存未命中的有效最大数量，则正确的抽象传递n，使得max（n，n）=n，即，n n.在这种情况下，我们说抽象语义过度近似具体语义。MP. Sotin等人理论计算机科学电子笔记164（2006）153165∈∈⎜⎜⎜⎜⎜.⎜⎜⎜⎜⎜.⎟⎟⎜⎟⎟⎟⎟为了构造抽象转换矩阵，我们计算抽象语义中的转换成本。例如，我们可以通过下面的案例分析来计算迁移（1，y）→q（2，1）的q• 对于ip= 1，我们有Instrat（m，ip）=loadτ x。• 对于任何转换s→qsJ使得ip=1in s，使得在高速缓存中访问的最后一个元素是y并且使得l.f.x C，我们可以证明q= 0并且s（resp. sJ）被（1，y）（resp.（2，1））。• 对于任何转换s→qsJ使得ip=1in s，使得在缓存中访问的最后一个元素是y并且l.f.x/C，我们可以证明q = 1并且s（resp. sJ）被（1，y）（resp. （2，1））。• 值q使得（1，y）→q（2，1）定义为：Q|s→qsJ<$α（s）=JS{（1，y）<$α（s）=（2，1）}，因此等于0<$1=max{0，1}=1。下面给出表示抽象语义的矩阵M。值的计算类似于上面的示例。⎛⎜⎜⎜⎜⎜1，x⎜1年，y⎜1，t⎜第1，1页⎞...二，一...3，t...四，一...5 x...六一 7，y... ⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎟⎜ ⎟M= 0。⎟⎜ ⎟⎜ ⎟2012年2月1日⎟2003年，⎜ ⎟4，1万美元⎜ ⎟15，000美元⎜ ⎟2016年6月1日⎝ ⎠7岁这个矩阵包含了很多次出现的值。此外，未示出的列和行仅为k，因此稀疏矩阵算法可以用于计算M在（N_{k}，max，+）中的传递闭包：从该矩阵，可以通过以下矩阵运算来提取具有ip= 1的状态和具有ip= 7的状态之间的全局转移成本cg：cg= I. （M）+.F = 3 <$2 <$3 <$3 <$3 <$4. ⊕⊥ = 3哪里• I是所有抽象状态的值为0的行向量，其指令指针为1，否则为0。• F是列向量，其值为0，用于所有抽象状态，其指令指针为7，否则为0。1，1⊥⊥⊥⊥⊥0⊥⊥⊥⊥⊥1⊥⊥⊥⊥⊥1⊥⊥⊥⊥⊥1⊥⊥⊥⊥⊥⊥0⊥⊥⊥⊥⊥⊥1⊥⊥⊥⊥⊥⊥0⊥⊥⊥⊥⊥⊥1⊥⊥⊥⊥⊥⊥0⊥⊥⊥⊥⊥⊥166P. Sotin等人理论计算机科学电子笔记164（2006）1531，2011 1 2 33⎜⎜⎜⎜⎜.2，1万0 1 123，时间 1 1 2 2⎟⎟⎟⎟.⎟给定的抽象为计算最大读取未命中提供了良好的结果，即 返回一个合理接近有效最大读取未命中的值。那应得事实上，大多数时候，一条指令的结果立即被下一条指令使用。⎛ ⎞我...二，一...3，t...四，一...5 x...六一 7，y... ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟1，x0 0 1 1 2⎜ ⎟2019年1月1日星期二上午10时30分⎜ ⎟电话：+86-11-223-3311111⎜ ⎟2019 -01 - 22 00：00：00⎜ ⎟（M）+= 0。⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎜ ⎟⎟⎟⎟⎟⎟⎟⎟⎟⎠6结论我们已经提出了一个扩展的操作语义的Java卡语言，模型之间的状态转换成本。这种语义是以一种通用的方式定义的，以表达各种类型的成本。语义域和转换集成了一个缓存模型，非常适合于评估成本，不仅取决于输入输出行为，特别是执行时间。作为实例化的一个例子，我们给出了附加到高速缓存未命中计算的成本将语义表示为半模上的线性算子允许通过矩阵运算来计算它。我们定义了两个不同的附加到程序的成本概念：只要可能，从初始状态到最终状态的全局成本使用语义的传递闭包M+计算。如果转换的底层图包含循环，我们可以定义一个长期成本，它给出了沿着转换循环的平均成本，使用幂等半环的Perron-Frobenius定理的变体。大多数时候，由操作语义定义的矩阵是无限维的。为了克服这个问题，我们定义了一个框架来将这种语义抽象为可计算的语义。具体语义矩阵和抽象语义矩阵之间的正确性关系保证了从抽象语义计算的结果是具体语义的过近似。最后，我们提出了一个抽象的例子，计算一个给定的程序的缓存未命中的数量的安全近似⎜⎜⎜⎜⎜4，1万美元⊥⊥01115，000 美元⊥⊥⊥112006年6月 1日⎝⊥⊥⊥⊥⊥07岁⊥⊥⊥⊥⊥⊥P. Sotin等人理论计算机科学电子笔记164（2006）153167相关工作目前的工作是基于Di Pierro和Wiklicky [7]开发的定量抽象解释我们遵循他们的方法在modeling程序作为线性算子在向量空间，但是，我们已经推广到考虑运营商是半模半环。这种概括的原因是，这种结构自然出现在成本分析中。与Di Pierro和Wiklicky的工作相比，另一个不同之处在于我们考虑的是一种低级面向对象的编程语言，而不是理想化的声明语言（概率并发约束编程和lambda演算）。这使我们能够研究各种（低级别）的定量属性，如缓存行为，但需要纳入状态抽象，这与用于分析声明性语言的抽象Alt、Ferdinand、Martin和Wilhelm [2]提出了一种通过抽象解释来预测缓存行为的方法.我们在不同的层次上工作，因为他们的论文集中在对缓存进行建模并对其进行适当的抽象。在我们的提议中，所有缓存模型都隐藏在函数更新之后，这仍然需要定义。他们的工作中有三点我们几乎可以直接在我们的框架中使用：各种缓存模型（例如直接映射，A-way关联）来实现我们的更新功能，它们的抽象域，以便设计我们的定量抽象以及它们对缓存和写入的观察，以便开发一个准确的模型。今后工作文中给出的费用计算实例是手工完成的。未来的工作包括在稀疏矩阵中实现传递闭包和特征值的惰性计算，这将允许有效和高效的计算程序成本。计算正确的抽象是一个问题，因为它通常是定量的抽象解释。我们需要开发一个框架，允许定义状态的抽象（通过经典抽象函数或等价关系），然后自动获得有限的抽象矩阵。使用Moore-Penrose伪逆的抽象定义具有很强的理论基础，但它在实际计算抽象中的应用需要研究。进一步工作的另一个问题是放宽正确性标准，使抽象估计“接近”（但不一定大于）确切的数量。这是可能的，因为我们在抽象属性空间上有一个度量，因此可以估计具体操作符和抽象操作符的距离。此外，为了评估影响，例如 对于程序转换，这类信息似乎是足够的。最后，值得研究的是如何将我们的框架与Aspinall等人定义的资源代数概念相结合。 [1]的文件。168P. Sotin等人理论计算机科学电子笔记164（2006）153确认感谢Guillaume Dufay对本文早期草稿的全面评论，并感谢裁判的宝贵反馈。引用[1] D. 阿斯皮纳尔湖Beringer，M.Hofmann，H-W.Loidl和A.莫米利亚诺资源的程序逻辑理论计算机科学，出现。[2] Martin Alt，Christian Ferdinand，Florian Martin，and Reinhard Wilhelm.通过抽象解释预测缓存行为。在SAS[3] 斯蒂芬·高伯特介绍了离散事件的动态系统。 INRIA Rocquencourt，1999年。[4] Java Card平台的虚拟机规范。http://java.sun.com/products/javacard/specs.html的网站。[5] R. Marlet在SecSafe项目（v1.7）中学习的JCVM语言。技术报告，2001年4月。[6] 彼得·普施纳和克里斯蒂安·科扎。计算实时程序的最大执行时间Journal of Real-Time Systems，1（2）：159-176，Sep. 一九八九年[7] 亚历山德拉·迪·皮耶罗和赫伯特·维基基。并发约束编程：面向概率抽象解释。声明式编程的原理和实践，第127-138页，2000年[8] 蒂莫西·舍伍德和布拉德·考尔德。程序的时变行为技术报告CS 99 -630，UCSD，1999年8月。