一种多轴运动控制的mpsoc互斥模型

一种多轴运动控制的mpsoc互斥模型

在大多数种类的电子应用市场中，多处理器片上系统（pmsoc）逐渐成为市场的主流。此外，公共存储器通信是pmsc通信的标准模式。对于一个复杂的MPSOC系统,任务间互斥成为一个必须高效解决的关键问题。随着新的互斥算法不断出现,原来的互斥模型不能较好地描述MPSOC互斥问题和量化互斥算法性能指标,鉴于此,本文在综合分析各种互斥算法和模型的基础上提出了一种共享存储器MPSOC互斥模型(SM-MPSOC-MM)。1传统互斥模型互斥算法用来确保在某一时刻,仅有一个任务访问共享资源。互斥模型意义在于用一种通用的方式来描述和评价互斥算法。文献在时空模型的基础上定义了事件,进而定义系统执行,并给出一系列概念、定理用于描述和论证互斥问题。定义1事件≡(x,y,t),事件在空间坐标(x,y)和时间t发生。定义2事件序列≡〈e1,e2,…,en〉。其中ei为事件,1≤i≤n。定义3a→b≡事件a先于b发生。定义4A→B≡∀a∈A:∀b∈B:a→b。定义5A┄>B≡∃a∈A:∃b∈B:a→b∨a=b。定义6系统执行≡三元组〈S,→,┄>〉。其中:S为事件/操作的有限集合或可数无限集合;→和┄>为S上的先序关系。定义7服务周期γ≡〈i,…,im〉,表示任务进入临界区的排列顺序(m个任务并发竞争临界区,任务i1首先进入临界区)。定义8ORD(γ)≡〈i′i,…,i′m〉。其中:i′1<…<i′m;i′1,…,i′m由i1,…,im经过一次循环排列而来。定义9CGV(cv,γ,ij)≡¬cv(ij-1)j>1。cv(im)j=1定义10CG(cv,γ,ij)≡cv(ij)≡CGV(cv,γ,ij)定义11CYC(i)≡{γ|∃i∈γ∧∃j∈γ∧i≠j}。定义12CYC(j,i)≡{γ|∃i∈γ:∃j∈γ:INDEX(γ,j)<INDEX(γ,i)}。定义13a*:=*b≡ifa≠bthena:=bfi。定义14await(p)≡while(¬p)do;od。定义15at(Li)≡是指任务i恰好执行到标号为L的语句前面。定义16in(CSi)≡当且仅当任务i执行到CS的开始、中间或结束(刚刚结束)。定义17A⊃B≡A逻辑蕴涵B即A成立,那么B一定成立。定义18□≡现在和永远都成立。例如,□(x>0):x现在并且永远为正数。定义19

≡现在或将来某个时间成立。定义20PQ≡□(P⊃

Q)。文献则将系统执行定义为如下三元组:定义21系统执行≡〈E‚Τ→,D→〉。其中:E为事件的集合;aΤ→b≡a在b开始前完成;aD→b≡a比b先访问同一个共享变量。结合各种互斥算法,综合分析传统互斥模型,其存在如下不足:a)抽象单位为任务,即不区别任务是来自哪个处理器、不能很好地描述区分处理器任务源的互斥算法。b)不能较好地描述任务优先级、实时性。c)未精确量化性能指标。d)未严格区分并行和并发,描述不够精确。2本研究的模式2.1pro、cv、ev上的关系为克服原来互斥模型的缺点,更好地描述互斥算法和量化互斥性能,将共享存储器MPSOC互斥模型(SM-MPSOC-MM)描述为如下四元组:定义22M≡(PRO,CV,EV,R)。其中:PRO(property)表示互斥模型相关属性集合,包括:P—处理器标志;PRI-P—处理器优先级;PRI-T—任务优先级;TAB—临界区申请开始时间;TAF—申请结束时间(即申请成功时的时间);TEB—退出开始时间;TEF—退出结束时间;PCS—临界区优先级(可根据PRI-P、PRI-T、TCS确定);DLCS—进入临界区的最后期限;TCS—临界区类型(N:一般;S:软实时;H:硬实时;A:可退出)。CV(communicationvariable)用于控制互斥的共享通信变量集合。EV(event)表示互斥相关事件集合,包括:EN—进入临界区事件集合;CS—临界区事件集合;EX—正常退出临界区事件集合;GU—放弃申请临界区而主动退出事件集合;AB—异常退出临界区事件集合。R(relation)表示PRO、CV、EV上的关系集合,包括算术关系、逻辑关系、第1章中描述的关系和以下扩展关系。定义23同构事件,即不考虑事件a、b发生时间,将有关处理器标志、任务标志和临界区标志部分进行常量替换后有a=b,那么称a与b为同构事件,记为aΗΟ↔b。例如a:readcv(pi)aΗΟ↔b:readcv(pj)。其中:pi、pj为处理器标志;cv为共享通信变量。定理1ifaΗΟ↔b,bΗΟ↔cthenaΗΟ↔c。证明如果aΗΟ↔b,那么对a、b进行同构事件常量替换后有a=b;同理,对b、c进行同构事件常量替换后有b=c,那么a、b、c全部进行同构事件常量替换后会有a=c,根据a=c和定义23可知aΗΟ↔c,证毕。定义24ψ(a)≡事件a的开始时间。定义25ζ(a)≡事件a的结束时间。定义26a→b≡ζ(a)<ψ(b)。定义27INDEX(A,a)≡a在A中的位序,如A=〈a,…〉,则INDEX(A,a)=1。定义28a↔b≡(¬(a→b))∧(¬(b→a))(原子并发)。定义29as↔b≡(ψ(a)=ψ(b)∧aΗΟ↔b)(原子并行)。定理2ifas↔bthena↔b。证明如果as↔b,根据定义29可知ψ(a)=ψ(b),由ψ(a)=ψ(b)和定义26可知¬(a→b)且¬(b→a),根据它们和定义28可知a↔b,证毕。定理3ifas↔b,bs↔cthenas↔c。证明如果as↔b,根据定义29可知ψ(a)=ψ(b),同理有ψ(b)=ψ(c),由它们可知ψ(a)=ψ(c);如果as↔b,那么根据定义29可知aΗΟ↔b,同理有bΗΟ↔c,由aΗΟ↔b,bΗΟ↔c及定理1可推出aΗΟ↔c;根据ψ(a)=ψ(c),aΗΟ↔c和定义29可知as↔c,证毕。定义30并发。A↔B≡(¬(A→B))∧(¬(A→B))。定义31并行As↔B≡(∀a∈A:∃b∈B∧INDEX(A,a)=INDEX(B,b)∧as↔b)定理4ifAs↔B,Bs↔CthenAs↔C。证明如果As↔B‚Bs↔C,根据定义31可知∀a∈A:∃b∈B∧INDEX(A,a)=INDEX(B,b)∧as↔b(1)∀b′∈B:∃c∈C∧INDEX(B,b′)=ΙΝDEX(C,c)∧b′s↔c)(2)将式(2)的b′给定值b,那么有b∈B:∃c∈C∧INDEX(B,b)=INDEX(C,c)∧bs↔c(3)由式(1)和(3)可知∀a∈A:∃c∈C∧INDEX(A,a)=INDEX(C,c)∧as↔c(4)根据定义31和式(4)可得As↔C,证毕。定义32扩展服务周期γ≡〈i1,…,im〉表示进入临界区的排列顺序。其中iw=ID(j,k,l),惟一标志处理器j的第k个任务进入第l个临界区(1≤w≤m)。定义33等待周期映射函数WCM(i)≡{γ|∃γ∈CYC(i),∀γ′∈γ:ifCG(cv,γ′,i)then(CSi∈CS∨CS=Ø)}。注意此处i为ID(j,k,l),CSi即CSjkl。定义34in(A)≡ψ(A)≤ψ(current)≤ζ(A)。其中ψ(current)为执行环境当前时刻。2.2sm-mpssc-mm互排斥算法的抽象2.2.1n-fmoc算法即控制器源如果在ENijk中,存在可选部分(中的部分)则称其为可退出型(abortable)互斥算法。根据μ映射方式的不同可区分不同组织形式的互斥算法。如果在r、μ、ID函数中,任务处理方式随处理器不同而有所不同,则称该互斥算法区分处理器源。如果仅存在一个υ,那么该算法称为自旋互斥算法。SM-MPSOC-MM互斥算法状态转换如图1所示。2.2.2任务阶段的时域定义ifCS≠Øthen∃!CSijk∈CS。任何互斥算法都需具有此特性。∃!:惟一存在。定义36公平性(firstcomefirstserved)ifENijk→ENuvwthenCSijk→CSuvw。更强的定义如下:if(ψ(ENijk)<ψ(ENuvw))thenCSijk→CSuvw定义37实时性if(PCSijk>PCSuvw)∧ENijk↔ENUVWthenCSijk→CSuvw定义38无饥饿(starvation-freedom)ifENijk∈ENthen∃t∈T,ψ(CSijk)=t,CSijk∈CS定义39无活锁(livelock-freedom)ifIJK={ijk|ENijk∈EN}≠Øthen∃≥1t∈T,∃≥1ijk∈IJK,ψ(CSijk)=t,CSijk∈CS无饥饿或无活锁能确保任务最终进入临界区,但不能确保何时进入。定义40无停工(lockout-freedom)ifENijk∈ENthen∃t≥ψ(ENijk)∈TENijk∉EN它能确保任务最终退出EN。定义41无死锁(deadlock-freedom)EN≠ØCS≠Ø或者in(ENijk)u,v,w:in(CSuvw)。它能保证系统源源不断地有任务进入CS,但不能确保每一个任务都进入CS。2.2.3根据sm-mpssc-mm互排斥算法1enijkcsijk,enijkenuvw的情况假设∃CSijk,∃CSuvw:CSijk↔CSuvw,那么一定有ENuvw→CSuvw,ENijk→CSijk,ENijk↔ENuvw(¬(ENijk↔ENuvw)⇒CSijk↔CSuvw的情况不满足式ENijk↔ENuvw,但可通过举反例证明)。根据算法描述发现ENUVW↔CSuvw,ENijk↔CSIijk,ENijk↔ENuvw与原假设矛盾,即可获证。2直接根据定义证明其他互斥算法特性的证明与以上两者类似,对于某些算法,直接根据定义证明也较方便。当某算法不满足某特性时,一般采用举反例的形式证明。2.3系统规模及sc东南角点到点可扩展度见表1为更好地评价互斥算法优劣,将算法性能指标精确量化为如下定义:N为竞争临界区的处理器数;Ti为处理器i竞争临界区的任务数;Cij为处理器i任务j的临界区数。定义42平均执行时间(¯EΤ)¯EΤ=Ν∑i=1Τi∑j=1Cij∑k=1(ΤEFijk-ΤEBijk)+(ΤAFijk-ΤABijk)Ν∑i=1Τi∑j=1Cij定义43平均响应时间(平均延迟时间,¯RΤ)¯RΤ=Ν∑i=1Τi∑j=1Cij∑k=1(ΤAFijk-ΤABijk)Ν∑i=1Τi∑j=1Cij定义44平均释放代价(¯RC)¯RC=Ν∑i=1Τi∑j=1Cij∑k=1(ΤEFijk-ΤEBijk)Ν∑i=1Τi∑j=1Cij定义45点到点可扩展度(系统规模从M变化到M′时)scale(Μ,Μ′)≡¯RΤΜ/¯RΤΜ′。其中系统规模:Ν∑i=1Τi∑j=1Cij∑k=11。定义46平均可扩展度S≡p∑i=2(i-1)×scale(1,i)p∑i=2(i-1)。其中:p为最大系统规模。定义47整体实时性(TRT)ΤRΤ=Ν∑i=1Τi∑j=1Cij∑k=1μ(ΡCSijk)×(ΤAFijk-ΤABijk)Ν∑i=1Τi∑j=1Cij其中:w(PCSijk)为临界区优先级实时性权值。3sm-mpsoc-mm模型为了最好地理解SM-MPSOC-MM模型,本章用SM-MPSOC-MM模型描述和论证了一个简单的互斥算法(读、写操作为原子操作)。3.1相互排斥算法sm-mpssc-mm描述3.2相排斥算法为sm-mpssc-mm1明确rp1l1,l1证明不失一般性,设p1=ID(i,j,k),p2=ID(u,v,w),CSijk↔CSuvw。CSijk↔CSuvw⇒Rp1(L1=0)s↔(Rp2(L1=0)(5)且Rp1(L2=0)→Rp2(L2=0)(6)由算法可知:Rp1(L1=0)→Wp1(L1:=p1)→Rp1(L2=0)(7)Rp2(L1=0)→Wp2(L1:=p2)→Rp2(L2=0)(8)综合式(5)～(8)可知,当ψ(Rp1(L2=0))(或ψ(Rp2(L2=0)))≤ψ(current)≤max{(ψ(CSijk),ψ(CSuvw)}时,L1的值惟一确定(p1、p2之一)(9)由算法可知Rp1(L2=0)(β)→Rp1(L1=p1)→Wp1(L2:=p1)→CSijk(10)Rp2(L2=0)→Rp2(L1=p2)→Wp2(L2:=p2)→CSuvw(11)由式(10)(11)可知,当ψ(Rp1(L2=0))≤ψ(current)≤max{ζ(CSijk),ζ(CSuvw)}时,p1读得L1为p1,p2读得L1为p2,这与式(9)矛盾,证毕。2p2p有执行语义证明假设¬(in(ENijk)∃u,v,w:in(CSuvw)),即in(ENijk)∧□(∀u,v,w:¬in(CSuvw))。其中:p1=ID(i,j,k);p2=ID(u,v,w)。——at(αp1)L1≠0—p1或者发现L1≠0或者发现为0便将其置为p1。——L1≠0⊃□L1≠0—L1=0只有可能是退出临界区的任务将其置为0,而假设□(∀u,v,w:¬in(CSuvw))。——□L1≠0∃p2=ID(u,v,w):□L1=p2—在对L1进行并发写操作的任务中,p2为最后一个。——□L1=p2(at(βp2))—L1=p2,很显然,p2能执行β语句。下面将分三种情况进行讨论:a)当βp2→βp1时,——at(βp2)L2=p2at(δp2)—p2检测到L2=0,将L2置为p2,然后执行δ。——at(δp2)∧□L1=p2false—p2执行δ,发现□L1=p2,因此p2可进入临界区,这与假设□(∀u,v,w:¬in(CSuvw))矛盾。b)βp1→βp2时——at(βp1)L2=p1at(δp1)at(ζp1)L2=0L2=0—p1执行β检测到L2=0,将L2置为p1;然后执行δ发现L1≠p1,转而执行ζ,将L2置为0并转到执行α语句。由于WL1=p2,只能不断地执行α。——at(βp2)at(γp2)L2=0at(δp2)—p2执行β语句,发现L2已等于p1,转而执行γ,于是再往下执行α、β,等到p1将L