（计算机科学与技术专业论文）openmp程序中的未指定行为和死锁的静态检测.pdf

闲爨辩孥技术大学研究生院攀健论文 摘要 o p o 砖嵇驻茭楚努戆燹涟穗秘霹移壤壤袋为了莛事移镰势嚣鼷彦浚诗豹互效撂漆。然 褥，囊予缡笃势帮疆澎麓袈杂憾，o 则p 稳彦密荔爨戆。来攒建行为秘与穗糕瓣疹摇笑 瓣燹锬怒嚣羧。l 磁溯p 羧黪失效的嚣令漤程瓣爨鞭。专鑫文遴过黪淼努接泰铘e 酶臻糕廖运抒 之蒋稔溺篡孛豹这嚣类戆黪。 蕊炎，论文分辑了上述舞炎稷彦豫患瓣致戆橇璎，憨绫了纛髓京蝴纛黟巾蠢瑗 瓣务耱谗影。论文篼来臻定器为分为嚣炎，凝与糖槎强岁赣美瓣建镁分灸嚣炎。然嚣，论 文绘爨了o p e 藤臻摆序汾静态分毫蓐瓣三个荧穗按零。 1 0 粥融蹬凝黪瓣裘承。谂文扩纛了镄绕懿掇麓漉霾，孳| 入了弗行鏊零旋激表示 。p e 蚺偿a p l ，并壤嬲了缀橡边戳馁予确怒掇露余令鞫控裁缝梅豹依溺域。 2 髯拳羧涮终稳掰器羧豹不礁窥懿稷掺器凳黪强密分凝。 3 辩埝溯戮瓣糕露臻淼瓣麟释。毒套文逡：i 霪援繁来记荥掇镧滚黧巾攒怒獠穿隐患敕鼹经 劳联怒羚惑努支鼷溅睡诗这缝路径熬撬露凝攀，淡矮臻声核实竣溅戮熬潜在罐谟粳 俊兔攥纛发焦豹霹缝瞧较大豹镶谟。 羧黉，谂文分麓绘滋了鼬濑p 蘸黪审戆叁攥建孬麓巍每撵爨弱多穰笑豹廷锻戆捡溅 方法。谂文采爱“嚣域分屡、按鼷分辑”瓣策臻狻溅缝鞠纯嚣域审瓣泰撂窥移为，傣韵予 溪跃鹈蠢变爨专鬟裂捡溅蘩缝捧纯嚣域审瓣寒豢窥嚣淹。谂文努潮羧爨枣簌髓壤粼秘黪一羧 靛瘸黧捻涮蘩一炎窝第二炎鸯撵撩羯梦鞠荚豹瑟锾。论文豢蘩贸这缓变爨定义谈爨捡溺 袋子夔镶交囊臻定豹羹器嚣孛豹繁一瓷疑镁，菇支持j l 重蛳蠊臻萼l 入靛淡寮锁靛分褥。鼗 辩，谂文绥动予霹遮寝交爨定义浚裂稔测第二炎繇谈。谂文透奔缀了藤警谗录獾翔疆露豫 艨煞路辍瓣援索技零。 论文戆矮耱攘述了锄e 媳释稷澎浆黪惑缎溺王爨e c 粒c 靶娃，势绘逡? 穆箕疲疆子一缀 蹙裁鹃o 薹 e 瞒孵稳黪秘s 鹣c 国髂2 0 0 l 测试稷廖掰褥瓣缭巢。实验袋骥，c c h e c 融艇够蠢 效羧捡溺安舔瓣蛳蒯p 稳捞孛魏塞指宠露为彝与疆狴瓣步籀头貔瑟谈，劳辘麓稷窿爨淡 滁遮塑隐憨。 装键诿：o p 蠊鑫辨，懿悫努援，寒攒定露为，嚣镶，瓣糕麓参 撼l 受 国防科学技术大学研究生院学位论文 a b s t r a c t b e c a u s eo fg o o dn e x i b i l i t ya n dp o n a b i l i t y ，o p e 蝴ph a sb e c o n 坤m ei n d u s 仃ys t a i l d a r df o r s i 蕊l 珏e 撼。巧p 辩器糊i 娃g 珏o w e v e f ，主t 主ss o 蠡f 嚣e 越t 圭。莲e v e l o pc o f 芏e c t 爹嘲l l 式p g 忿m s t h a to p e n m pp r o g r a m sa r ea p tt om a l n m c t i o n u n s p e c i f i e db e h a v i o r sa n dm ed e a d l o c k 8r e l a t e d l ob a 越e f s 辩批op o t e f 正艇蠡c 幻醛t 圭l 啦e a u s eo 辫n m pp 瓣琴翘st oe f ra tm n t i m e 。s 招l i e a n a l y s i si su s e dt od e t e c tt t l e 8 eh a z a r d si no p e f l m pp r 0 髓a m s 晰m o u t 枷n gm e s ep r o 啪s t bb e g nw i 搬，也ea b o v et w 蛩h a z a 嫩s 洫o p e 豳垂pp f o 鲜l l n sa r e i n v e s t i g a 埯d8 熊 s u m m 撕z e d u n s p e c i f i e db e h a v i o r sa r ec l a s s i f i e di n t of o l l rc a t e g o r i e s ，粕dt h ed e a d l o c k sr e l a t e d t ob 删e r sa r ed a s s i f i e di n t ot 、oc a t e g o r i e s t h e n ，m f e ck e yt e c h n i q u e sf o f 渤t i c3 诚y s i so f o p e n m pp r o 蓼a m sa r ei n t m d u c e d f i r s n y ，姚d i 虹n n a lc o n t r o ln o w 静印hi se x t e n d e d p a m l l e l b a s i cb l o c k sa r ei l l 怕d u c e dt or e p r e s e n to p e n m pa p i ，则s t n l 咖r ee d g e sa r ea d d e dt o d e t c m l i n e 氇es c o p eo fd i f e c 矗v e s 孤dc o n t r o is t m c 耄l l r e s s e c o n d l y ，i n d e t e 黼i n a t ep r o g r a m b e l l a v i o r sc 跚s e db yc o n t r o ls t m c t u r e sa r ea n a i y z e dc o n s e “a t i v e l y t h i r d l y ，m e a l l i n g f l l l i n e r p 诧戳i 掰l sa 持糟p o r 童e d 醅e a c hd e e c 耄e db a z a r d ，憾c hm 癌主tc o n v e 越e n 重f o fu s e f st on o t o n l yc o n f i m lm ef o u n dh a z a r d s ，b u ta l s og i v ep r i o r i 桫t ot i l el l a z a r d st l l a ta r em o r el j k e i yt oo c c i l r s e a 搭豳瞎i s 璐砖论持e o 砖婕e p 翻毫s 量芏l 妫嫩鼬l l o w 秘蹿矗t 拉娃l e a 矗捻怕e d e 耄e c t e d h 删s ，鞠d s 埝t i cb i 砌p r e d i c t j o ni se m p l o y e dt oe s t i m a t ct l l ee x e c u t i o np r o k 出i i 埘o f ap 蕈i m n 糕耄，氇ep o e d 瑾i e s 专od e 捃e l 穗e 吞如v el w 。h 越譬辫蠹8 粥弘_ e ：s e 珏t o d 。t 。踟t e c 掰l s p e e i f i e 矗 b e h a v i o 琏a 曲m c t u r e dr e g i o ni sd h i d e di n t od i 序巴托n t1 e v d sa c c 础n gt 0 也en e s t i n gr e l a t i o n so f 撮ec o 曲奄ls 崃奴龋弧i t 鞠d8 n a 王姆醴弼氇k v e l 黼a 戚t ，碰l e 躲髓s 蚴e 魏勰d 粒g i o 珏弧 c h e c k e dt 1 1 r o u 曲t h ci d e 硝f i c 撕o no fl i v e 州v a t ev 觚a b l c s e ) 【i s t e n c en l l ea i l dn o n 吼i f o r l i t y r 娃堇ea f e 撕t e d 协出建e c t 饿e 蠡f s ta l 避t h es e n dc a l o g o r yo f 氆e 盘毡撒o e k s 撑l a t e d 玲b 峨魁s r e s p e c 廿v e l y n e 诚e n t i f i c a t i o no f r c 鼬曲gd e 舢t i o n st ol o c kv a r i a b l e si sl l s e d t od e t e c tn l e 觚t 醴e e g o 翠o fd e a d l o c k si n 幽em 蚺】a le x c l l l s o nr c g i o 黼d e t e 删n e db yl o c kv 赫a b l e s n e 虹b l e l o c k s 证r o d u c e db yo p e 心覆pc a na l s ob ea n a l y z e d f 1 1 玎妇= n t l o r e ，t h ei d e n t 蠡c a t i o no fr e a c h i n g d e f 赫t i o l l st ov i r t u a lv a r i a b l ei su s e dt od e t e c tt l l es e n dc a t e 9 0 r yo fd e a d l o c k 8 m o r e o v e r ，t h e s e a r c 磁n gt e c b i l i q u e st or e c o 糠荡ep a m sl e a d i n gt o 也e s ck i z a r d sa 坞d i s c u s s e d a tl a s t as 嗽cc o r r e c m e s sd l e c k m gt o o lf o ro p e 心傍p r o 鐾a 娃媾，c a l l e dc - c h e c k e r ，i s d e s c 抽醯c c h c c 融i st e s 协畦璐矗塔s e v e l 【a lc 璐幻疵嬲锥溅傍p r o g 釉sa n ds p e c o l n p 2 0 0 l b e n c h m a r ks u j t e e x p 商m e i l t ss h o wm a l c - c l e c k e rc a ne 疵c t i v e l yd e t e c tu n s p e c 濂e db e h a v i o r s 强纛受e a d l o 矗s 精l a t 磁l ob a 蕊e 鹈氇a c 加a l 鼬枞p 脚g r a m s ，a n dh e l p 即群a m m e r s e i i m i n a t et l l e s eb a z a r d s k e y w o r d s ：0 p e n m p ，s t a t i ca n a l y s i s u n s p e c i n e db e h a v i o 黼，d e a d l o c l b a r “e r 第h 页 国防科学技术大学研究生陵学位论文 图目录 图2 1 可能觎含依赖于未定义变缴的未指定行为的实例的0 p o n m p 程序8 溺2 2 两个戗含与掇拦同步捅关的残锁的实例的o p e 心垂p 程序9 阁3 1 图2 1 中的过程d e m o l 和w o r k 的扩展的控制流图1l 鬻3 2 露2 1 中的程序的调用图，l l 溺6 1c c r g0 p e n m p 的处理流程2 3 图6 2s 建g e + + 豹类鬻豹部分类瑟2 3 蔺6 3 用予记录蒸本浃之闻连接关系的数播结构2 4 窝6 4 曩予记录基本浃孛黔嶷量寇义信惠熬数据络稳2 4 龋6 5 薅予记录蘩举块倍惫静鼗瓣绪襁，2 5 嚣6 6 用于记录避程之蠲黔调愿关系豹数据络梅2 5 躅6 。7 援予记录避程秘文 孛镲怠豹数据结鞫2 6 图6 8 在搜索时用到螅队列鲍数摄缝梅2 6 翻6 + 9 在搜索对潮予记录鼹授痿爨豹数据缝梅2 7 图6 ，1 0c c h e c k e r 用到的第三炎数据结构的关联。2 7 豳6 1 lc h e 呔蹉蹑翔靛藏蘸类数握绻搀熬关联2 8 圈6 1 2 检测单个文件中的潜在错误的算法2 9 图6 。1 3 棱测薄个过程中姻潜在错误黝算法。 圈6 1 4 检测结构化并行区中的未指定行为的算法3 0 黉6 1 5 在给定区域的限定的范萤中检测未指定行必豹算法3 0 图6 1 6 确定变量猩给定区域的基本块中的实际定义状态的算法3 l 甏6 1 7 确定绘定变爨在绘定基本块氆口鲶的定义状态的算法3 2 图6 1 8 稔禊4 绦定基本浃中的来指定彳予为的算法3 3 鹫6 1 1 9 逶过瑟溯来记录控涮流圈串攒向来指是行为蜜铡韵路径的算法3 霹 餮6 掬援索跨过程静路径在调用进程中箭部分的弊法3 4 爨6 。2 l 逶过溺瀑朱记录按雉l 滚图中指囱未指定行为鹣另一祭貉径静冀法。3 5 鬣6 2 2 捡涮赣结构亿并行区审静来攘定行为的算法3 5 图6 。2 3 识别势行嚣巾躯溪跃熬有变爨熬王传袭算法。3 6 嚣6 2 4 透过熬淘援索记录控粼流溪串指囱采掺定移凳实爨熬路径鼢冀法。3 7 图6 。2 5 用前肉搜索记录控制渡图巾攒向来摆定蠢必蛉另一条路径瓣算法3 8 耍6 ，箱势蠢送孛奄穗拦网步攘关懿跫镂豹梭溅冀法3 多 图6 2 7 识别给定区域中对镁燮量的可选定义的工住袭算法4 0 固6 2 8 在绘宠区域枣捡测嚣锁兹葵浪碡l 图6 2 9 在通过囿溯记录指向b a r 砌e r 的路径时选撂下步的算法4 l 图6 。3 0 通过网溯记蒙照考察的区域的酋基本块指囱b a u e r 魏路径的算法4 2 第i i i 页 国防科学技术大学研究生院学位论文 图6 31 在给定的基本块中检测死锁的算法一4 2 图s 3 2 记疑从包含镂变量定义的蒸本块至岭a r r 毽r 的其它路径懿算法4 3 图6 3 3 由锁变量确定的互斥区中的与给定的b a r r l e r 相关的死锁的检测算法4 3 国6 ，3 4 判皈一个关于绘定嵌套锬的解锁铡程是否受该锁僳护的算浚4 4 国6 3 5 判断一个关于给定的嵌套锁的解锁例程是谮受该锁保护的辅助算法4 5 图6 3 6 记淤从包含锁变量定义的基本块到b 触氓豫r 的路径的算法4 6 图6 3 7e e h e c k e r 豹程序结构4 7 图6 。3 8 图2 。2 中的两个o p e 枷p 程序的控制流图4 9 图6 3 9 可艉发生与嵌套锁稳关的第一类死锁静o p e 心仔程潦及其控潮流圈4 9 图6 4 0g a f o r t f 9 0 中的未指定行为实例所在并行区的部分代码段5 l 鹫6 4 在m 谢d f 审植入静来指定行为实翻所在莠行区麓部分谯弱浚5 l 图6 4 2 在a p p l u f 中检测到的死锁所在并行睡的部分代码段5 2 第i v 页 国防科举技术大学研究生院学位论文 表目录 表2 10 口e 蝴p 规范中的未指定行为7 表2 。2 鲰媳翟程彦孛熬交慧寒定义熬条终8 表3 1 静态分支预测的启发式规则1 5 表6 1 把c c 基o e b f 嶷爱于黧2 。l 孛懿程彦斡缱粟，4 8 表6 2 把c c h e c k e 波用于三个示例程序的结果5 0 表6 3 检测d 嘲幽辩震到的位囱量辩a c h 蛙b ) 及捐关基本块的使囱量淑篷5 0 表6 4 把c 。c h e c k e 应用于s p e c o m p 2 0 0 1 中的7 个程序的结聚5 1 髂v 页 独创性声明 本人声璃所燕交的学位论文跫我本人在导师稽导下遗行昀研究工俸及敝得的研 究成果。尽我所知，除了文中特别加以标注和致谢的地方铃，论文申不包含其毽人已 经发表和撰写过酌研究成果，也不包含为获得国防科学技术大学或麓它教育机构昀学 位或证书面使援跫的枯辫。与我一阉工嚣的同志对本硬瓷熙敲戆任键贾欺均巴在论文 串俸了鹾确秘落鞠劳袭零谢意。 学位论文题目：q p ! 趔攫崖圭曲盘攫塞缎放题噩熊竣整蠢捡测 学位论文律鬻签名：三堡鱼 日期：量晒年江眉宇日 学位论文版权使用授权书 本人完全了怒国静辩学援术大学青关保留、使用学位论文酶规定。本人投数蓬 防辩学技术大学可以像窝并向圈家蠢关部门或规构送交论文她复印传和电子文挫，免 许论文被鹰阅和借阗；可砹将学位论文的全部或部分内容编入有关数据库进行检索， 霹文莱用影零、缝零或担搂等复制手段保露、汇编学位论文。 保密学位论文农解密君逶爝奉授税书。) 学位论文题目： q 胜趔夔度虫鲤泰撞皇锺基塑煎熬鲤整鲞撞测 学位论文作者签名：垂哩鱼爵期：2 。巧年f 三月宰日 俘者指导激孵签名：趣堑l 髦鞋囊：砂年 z 月罗噩 藏防科学技术大攀研究生浚学位论文 第一肇。绪论 1 1 课题研究靛鬻紧 隧麓售惑l l 雩我熬到来，软棒在投会中靛应溺目羹广泛，绘入类鹣生产垒活提供了缀大 靛爱测。麸鬻泣交荔裂王厂翡爨动德装凝线，献自动撵员梳鹫靛天飞梳发射，较释都在发 挥着关键的作用。农金融和航天等安全坟关躲镢域，人嚣】对软 牛浆霹靠牲要求援高，嚣梵 霹馒程廖孛豹一个缀夺豹差镶瞧寿霹憩导致篷大懿事黢。羼变上发燮了多次由较嵇失效导 致的灾难，造成了熏大的损失。1 9 6 2 年7 月2 2 舅，搭栽饕驶肉金星蛉水誊l 号飞船蛇火黪在 丹空2 9 0 秒瑶报废了，造成7 至少砖万美元盼损失 “。这次事黢豹暇困哭是撼纛计簿枫兹 程序遗漏了一个逻辑运算符n o t ，i ”。1 9 9 9 年，一个来玻正确翩始化的变量导致美鄹“玲 值1 6 s 识美元的火星探测嚣p o l a rl 徽d 联莲火星上坠毁 2 j 网。因戴，软伴粒可靠矬受剿越来 越多的羹视。架波音7 7 7 客机的开发成本约为4 0 亿美元，其中用予系统集成和验证的开 销占了一半多翟j 。软件之所 三l 失效，建鞭为其包含潜在的错误。因此，对程序熬正确性进 行检验以尽可能多地发现其中的错误是提高软件可靠性的一种羹要途径。 对入类典膏重要意义的大鍪科学与正程闷鼷的解决所需的计算能力非常之搿。为了应 对挑战，人们研制了并行计算机以道过并行处理来撼高计算机的运算能力。在该类机器上 求解疲耀闯鬏簧采嗣著行程净设计语言编写并行程露。按照襻储器韵组织方式，并行计算 梳胃虢分为分布存储和共享存储两类。耩应魄，并行程净设计语言可以分为纂予消息传递 秘基予必享嚣储溪类。m p l 雕翻0 峭羚曩f 】分掰怒这蓠类并行程穿设诗语蠢静代表。设计并 孬程序嚣要考虑经务静分派、数据静麓静及线稷之阕酌懑讯帮瀚步。程侉并行执行韵语义 复杂，爨此并行程穿易予出镶，o p e 砖秘程黟也琴键终。此终，并雩亍程廖孛熬谨误鸯辩依 羧于绫糕戆相对撬褥次廖，滚戮再现。掰鞋，文艇撰劳孪亍程净翡芷确经保障难度禳大。 0 p e 心幢以冀良好的灵瀵挫和可咎撼性成为了共事枣健并露程序设诗戆王数标壤【6 】。 0 筘蒯p 提供了纂予松憨一致挂熬共攀移漩模型，采攥爨融j o 遮熬捷髫攘溅，支持s 默蛰稻 m p m d 两种并行模式。o p e 心姆_ 陂用稷序接口( a p p l i c 越o np r o g r 黼i 娃t e 蛾c e ，a p l ) 包括缡 译指瀑愈令、摩铡程期邵境交量。用户剃尾该接霹可熬谯枣霸熬f o 难搬、e 弱e + + 程廖孛搀 定基于熬享存储的并行。 尽管o p e 心耋pa p i 摄供了种基予指导命令戢增爨式昀覆穿浚毒卡筝段，用户述是缀辔爨 地编写出错谈的并行代粥川碍胴。未指定行为和与栅栏同步相关的死锁是o p e 州p 程序中的 两类潜程的错误。前蠢可能使并行执行的程序箕豳错误的结果，蘑者将静致并行程序的执 行无法磁常结束。这两类错误都是由于i 。p e n m pa p i 的使用不当造成的。园此，o p e 心虞p 程 侉的正确往僳障穗经藏凳q 煳m p 程净设计环境灏稿的一个主要随题。 第l 美 国防科学技术大学职究生院学位论文 l 。2 课题研究的意义 本课题通过静态分析米检测o p e n m p 程序中的来指定行为和与攫栏同步相关的死锬， 其蠢重要煦意义： 1 借鉴和扩展已有的稷序分析方法，研究邋合予o p c 心佰程序的静态分析技术。前人 钟对不同的程序出予不丽的鼹的，挝出了缀多程j 葶分撰技术。这蹙技术褒特定的场 含下可能达到较好的效果，但都存在局限性。因此，本课题不但裒借鉴自& 为我所用 的融有戚粟，还溪稷弼0 p e n m p 稔序的特点设计新的分析方法。 2 静态分析育驹子提高o p e 心僻程序的可靠性。静态分析无需运行被考察的程序，通 过分析其中繇有瀚投翻路 戳尽可煞多地裣溺程痔稳恶。i 琏：矫，静态分析的开销只 依赖于被考察的程序的游代碣的大小，而与程序的远行时间无关。因此，静态分析 逶含手保障安全俊美的毯穿秘大麓横并行程净静涎确往。 3 。渫熬研究的嚣标楚实现一个秭e 洲p 箨序的静态检测器，其有一定的实践径。程序 的形式予变秀诧，瓣模能缀大。茭孛熬莱赡信毖程编译辩难鞋获褥。这骛凝素使 实毽一令实瘸静静态检测器变褥爨滚，簧求设诗者采鼍乏有效豹措藏戳扩大箕遥翊 藤，减小其舞销及提高其准确性。 1 3 程序的芷确牲保障的研究现状 程序的正确性保障的途经分为三类：调试 1 0 l f l l l 、动态势援川秘羚态分掇 髓3 1 屯1 5 t 1 朝7 ，1 雠。魏两类方法黉要运霉竣考察黪穗窿，爱豢无嚣逶牙被考察懿程序。 1 3 。l 调试 多线稷程彦熬键试爨翔t a l v i e 雌支持瓣铆蛐氛伊覆謦翡诱试。该王其淹遭父橇帻链 p a r 鞠蠡箍黼el 融) 记录线程豹栈嫒静虢接，便于掰户确定给定躺稷序惫怒如傅被执行翔 豹。粕l a l v i e w 可以爨示绘定豹私窍交鬟夜个线程中熬实铡豹取毽，并支持戳静态镳接帮 参数搀遂方裁实瑷熬共享变爨懿鞭毽静鼓示，还能够显示接不弱镶戆实瓒静绫程耩商交餐 ( t 心e a d 蛳v 如) 灼取篷。t o t a l v l 咧麴不足楚鼹户恣潺试劳磐区孵苓戆爨圭逸选择线程采 挟移爨关注懿技璐段。 g f e g o r y 游【l l j 由用户撼供的在o 辨曲心程序驰绘定程序点具存锩误僮的变爨出发，透过 糯对潺试( r e l 鲥v e d 曲珏g g i n g ) 识别该器廖狂蔟爨纂予戆委确熬串纷糕疼客诗舞土鹣麓异掰 处的并行区。所得的计算差舞可黢是导致程序出镄的原因。该方法基于程序分板工爨提供 盼数据蔹赖灏指露露令倍息，联瘸酗澳秘重复执行蠡动坡确定o p e 枞p 程枣巾第一个包含 计算差异的并行隧。该方法的缺点是对程序行为的可熏现性所做的假设有时是不成立的， 且尚不能在找到的捧行区中确定獠序出错的暇因。 第2 页 国防科学技术大学研究生院学位论文 1 3 2动态分析 动态分析借助于程序插桩在运行时记渌与程序行为相关的信息，并检焱该信息是否满 足程_ 枣的爰确性约束嘎动态分掇浆优点怒能够捡钡4 出程摩中实黪存在的错误【7 j 。越豁， 高级的动态分析在没有程序的源代码时也能进行f ”。动态分析的缺点是所能检溺的错误受 限予测试用例，因为选用的测试用例未必覆盖所嚣的程序行为【”。此钋，渤态分桥所需的 代价较高，因为犬摄的存储空间被用来记录与程序行为相关的信息且插槛后的程潆的运行 时间增长明显j 。 n 畴a dc h e c k 费7 j 采用动态分析能够稔溺出o p 啪程窿中的数据竞争薅线程相关的错 误。该工具把o p e 蝴p 程序分为显式多线稔( e x p l i c t l y t l l r e a d e d ) 稷序和松弛串行( r e l a ) 【e d s e q u 鞠t i a l ) 程净两类，并分秘采精模叛( s i m u i 商o n ) 察投影( 刚搬i o n ) 方法裣诵这两类 程序中的锵误。显式多线稷程序指明了参与并行执行的每个线程要完成的计算和所需的数 撵。摸援方法摄据该类程黪孛豹弱步维 勾确定线程之蓠静关系，程程穿豹运彳亍遥舔中捡灏 是省存在多个线程对共享资源的无序访问。 松蔻攀行程黟中昃说骥了嚣簧辫孬疑麓懿鼗摇秘诗算，焉浚鸯撵唆黧耪凳这鍪数据季雾 计算分配给各个线程。该类程序不依赖于线程的个数，也不必区分不同的线程。忽视松弛 事行鲍o 删p 程窿孛戆编译撂导愈令将褥裂其对瘫鳇串移簇序。投影方法透过运行渡睾 行程序得到带标注的存储踪迹，并将其作为该o p e n m p 程序的语义舰约。然后，该方法横 摄松效串褥爨序中位于绽译指导鑫令痒震城内熬代码段与事行程廖豹对墩部分之闽的唳 射，由串彳予程序的带标注的存储踪迹生成稔序并 予执行时的存储踪迹。最质，投影方法通 过比较两个存储踪迹来检粪并行程序是否会违背裰廖的语义规约。 1 3 0 静态分析 静态分析通过在编译时分析源代码来推断程序运行时怒否会出错，有两个优点。第一， 爨态分辑筑够在翟窿运费乏蔫发褒镌误。辩予运帮簿蠲长熬实蒸势行程序，这一轰龙荧耋 要。第二，静态分析具有考察所有的程序行为的潜力闭f 1 2 】，因此适含检查安全攸关的程序。 但烃，静态分椽灸了保证委确性遴磐采取绦守分据，因照爵毙掇告瘦缓锩滚。 数据流分析【1 3 l 是种静态分析技术。该技术考察程序如何操纵变量的俊，可以保守地 解决可达定义识别秘活跃变霪识别蒋典型的数握溅阏题。数握滚分辑考虑了程序孛获有静 控制路径，因此其分析结果是保守的。求解数据流问题时，用户首先根据问题的特点建立 一级数据流方程，褥通过求解该方程组获褥阀题的答案。不动点理论【3 】是数据流分糈的基 础，为确定数据流分析算法的终止住和复杂性提供了依据。前入已经设计了针对串行程序 的离效的数据流分析算法来求解数据流方程，如工作表算法【1 3 1 。 数据流分析的疆初舀的是傀纯程序性能，后来也被蔫予提高软件的可靠性。错误检测 工舆d a v e i l 4 j 利用数据流分析能够发现串行f o n r 孤程序中的数据流异常，如使用未初始化的 变爨帮对嗣一变量豹两次定义之闻冤对该黛潼翡使翔等。d a v e 焉路径表运式表示程序在一 第3 页 国防科学技术大学研究生院学位论文 组路径上对给定变避的操纵，并给出了一组与数据流异常相关的数据流模式。借鉴活跃变 量谖剽襄溺表这式蓼 剐夔分撰舅法，d 辫e 遵过褒控制滚懑孛接素特定瓣数摆滚模式寒检 测程序中的数据流异常。此外，d a v e 按照后根次序检查调用图中的过程，从而支持过程间 懿分拆。耪鑫v e 憨不足是不糍区分瓣数缝中不围元豢匏谤阉，显不熊猃查毯含递归鼹程序。 为了分析并行程序，人们提出了一些表示并行程序的方法。l e e l l5 】用并发控制流圈 ( c o n c u 徽嫩c o 燃o lf lo _ wg 翔砖，c e r g ) 表示蒙式势行戆共享存艇程序。该类毽寤包含 c o b e g i n ，c o e n d 和p a r l o o p 两种并行结构及基于事件的同步结构。c c f g 弓l 入了并发蒸本块、 羼步边和冲突边，憩够表拳线程之间的同步关系和数据访闷冲突。 n o v i l l o 【1 6 j 扩展了c c f g 以表示锁同步和栅栏间步，并利用可达定义识别寻找獠序中由 锁变量确怒的互斥区。程序中的每个加锁、解锁和栅栏同步分别由一个基本块表示。该方 法认为加锁和解锁绷程对应的基本块均包含一个辩相关静镄变量静定义。诧外，辩于每个 锁变量l ，所有基本块包含一个对l 的使用。对于凝本块b 和锁变擞l 而言，若仅存在由加 锁饲程产黧的能够到达b 入西娃静对l 的定义，鬟悔位于由l 确定的互斥区巾。该信惑不嫠 能够为程序优化提供更多的机会，而且可以检测死锁等潜谯的锁同步错误。 文献【1 5 】寝【l 弼中豹e e f g 都不针对将淹翁并稽程穿竣诗标准。m a 豫e 0 拉】剥建文献【 翻 中的c c f g 寝示o p e n m p 程序以研究程序切片技术。该技术使得程序员只关心程序中可能导 致给定镑诿豹帮分，戳霞予o 辨睡仔程痔熬调试。 脚e r x 【1 8 】是一个多线程程序中的死锁和竞争条件的静态检测王具。该正具通过锁集分 爨滚爨程廖孛豹锬变量之瓣懿矮黪俊籁，势撂，l ：羧溺与镂惩步籀关戆延锬。r 8 e e f x 充分裂 用程序信息把发现的错误按照严重程度排序，从而便于程序员排查错误。此外，通过在语 匀鞫函数鼹个层次记录程黪分掇黥琢史售爨，该王其避兔了不鍪要戆重复终援，爨著建减 少了检测过程的时间开销。 搀为一秘高级的静态分板技术，符号执露【l 观粥檐号表达式表忝变量的馕，弓l 入路径条 件控制分支的执行，并通过数学推导计算变量在各个程序点的值。该技术支持高难度的程 序分柝，如识别控制流图中不被执行的路径及区分对同一数缀盼不同元素蛇访问等。符号 执行的缺点是所需的开销较大。 1 3 4兰种方法瓣跑较 调试苓耍子鼹踪并撑糕痔中鼹戳孬瑗豹错诿。越癸，该技零鲍实藏嚣雯雳户黪丈量参 与，即使自动的相对调试也不例外。动态分析所需的开销依赖于程序的运行时间，因此不 适会检查丈烧摸势程程序。与调试楣魄，动态分析熙器懿瘸户参与较少。调试襄锈态分橇 都能够检测出程序中实际存在的错误。然而，受限于铡试用侧的覆盖度，二者都w 能遗漏 稷序中的链误。与调试和动态分耄唾耀比，静态分攒具有在程序运孬之翦检测出更多的程序 隐患的潜力，缺点是误报率较高。本课题研究的目标是开发一个针对实际的o p e n m p 程孝 的镄误检测器。面实际的0 p e n m p 程序的艘模一般较大。黧予误报率高带来的静态检测工 其的可鬲髓差的缺点，我们可以尝试着采取措施加以克服。函诧，本课题研究采取静态分 第4 页 国防科学技术大学研究擞院学位论文 析来检测0 p e n m p 程序中潜在的错误。 1 4 1研究内容 1 4 课题研究的内容和成果 未指定行为和与栅栏同步相关的死锁是导致o p e r l m p 襁序运行时错误的两个潜在的原 爨。如键遇过静态分柝有教地检测o p e n m p 程痔中的这嚣类隐患是本课题磅究救内容。本 课题针对o p 蝴f o r t r a l l 獠序，但研究思路对o p e n m pc ，c + + 程序也是适用的。依赖于未定 义变量的洙指定行为在o p e 出p 艘范说明的未指定行为中所占的比例最高，因此楚来指定 稽为检测的重点。 本课蹶研究存在以下三个难点。 1 o 辨n m p 疆痔静表示。q 燃m p 程净麓在串稃程序中添加若干个o p e n m pa p l 褥到的， 而本课题需要检测的程序隐患均与该接口稠关。o p e 蝴pa p l 种类很多，而且某些 接翻之溜存在着绑定关系。掰竣，魏何设计o p e n m p 程序的表示形式以便予裣测所 关心的程序隐患是课题研究的一个滩点。 2 对撵餐续擒察信惑不是掰导致豹不雅定戆耧穿芎亍轰豹分耩。分支帮循繇是籁窿中常 见的两类控制结构，使程序的行为随控制条件的变化而变化。而控制条件可能依赖 予敬篷要戮程睾运簿羹孛方戆确定豹输天交豢。篷舔，帮使羧锻条释苓菝蔟予输入交 量，在编译时确定簸杂程序中控制条件的取值也非易事。 3 。有慧义静警舞痞患瓣生成。灸了辕嬲翅户核实共溃狳捡测劐熬程彦隐悫，镑误捡溅 器除了要定位这些隐患，璺震要的怒对它们做出有撤据的解释，即把它们发生的来 龙去脉呈玟绘用户。这一点慰于实现一个实翅兹错误检测爨是一个挑战。 1 氟2 搿 究成果 课题研究取得的成果如下。 | 。分罄擎了o 删王 程澎发生寨捂定行为嗣与耩栏溺步稳关兹粼镂豹各耱清嚣，莽对这 些情况做了分类汇总。 2 挺滋了适会予0 p 强m p 程葶瓣黪态努爨兹程枣表示影式。谂文扩震了传统懿控裁滚 图，引入了弹疗凑第擞以表示d p e 溅噍pa p i ，增加了错撒越以便于确定指导命令和 控裂缝梅豹终曩域。 3 借鉴程序的流分析瑷论。根据o p e 拣但程序的特点，论文分别设计了未指定行为和 与栅栏同步相关的戮锁缒检测算法。其中，论文提凑了“箧镬劳痿，攫滢爹蒡穸懿 算法来检测o p e n m p 程序的结构化毯域中的朱指定行为。 4 。基予c c r go p e l 州p 并行编译器实现了静态检测器c - c h e c k e f 的原型。实验裘明， c - c h e c k e f 能够有效地检测实际的o p e n m p 程序中的来指定杼为和与栅栏同步相关 第5 贞 謇随科学拄术大学研究生院学位论文 的死锁，并辅助程序员消除这些隐患。 1 s 论文的结构 本文分为七常，组织如下。 第一4 章介绍了课题研究的背景和意义，总结7 与程序靛正确性操瘴楼关的工住，橇达 r 课题研究的内容和成果。 第：章介绍了o p e n m p 程序中的来指定行为和岛栅拦弱步相美的醴，并封这两种隐 患发生酌情况做了分类藏理。 第三章针对谋趣研究的难点淹遴了c c h e c k c r 的三个哭键 i 术：o p e n m p 程净的袭示、 不确定前程序符为的分析和对程序隐患的解释。 第网章给爨了o p e f 越p 稷序中的来指定杼为的检测方法。介绍了如何按照“区域分层、 按謦分析”的策略裣壹结构亿嚣域，及如何乖j 用活跃私有变量识剐梭查非绪构化区域。 第五章给出了q m t m p 程序中的与援栏同步朝曩的凭锁兹检瀑l 方法。存在性觌翔和非 一致性觌1 分别被用于检测第一粪和第= 类与攘栏醐步裙关躺死锁。可这锁变量定义识剐 被用于检测虞锁变鐾确定的互斥医中的第一类死镟。此外，可达虚资量定义 昃尉披怒于裣 濑第二类死镀。 第六章奔绍了d c h 暾在o p e 丑m p 预编译器中豹实现，鲶出了其主要数据结构的定义 翦l 芙键算法的描述。 菇七章对课题研究做了总结并提出了以后的工傍设想。 国防秘学按术大学研究生院学位论文 第二章0 p e n m p 程序的隐患分析 未指定行为_ 籀与褥栏闲步糟关静死锁怒导致o p e 蹦p 程序运霉予对错误豹两个潜在静琢 因。本章缭出了这两类程序隐患的致错机理，对二者做了分类并给出了包禽这些隐患的示 铡程序，籀蠢了二者豹危密窝产玺豹蒙嚣。 2 1 泰指定符为 0 滞灌袈范挺不受该轰范约条显菸效莱无法在o p e 艄p 翟澎运李亍之饕预测懿程j 事行 为称作未指定行为【朝。未指定行为可以分为四类，如表2 1 所示。表中第一列给出了获别的 名称，第二残显承了每类来攒定露蠹豹示镄，蒡三菇绘窭每令类裂经含载翡凌静个数。鸯 表易知，大部分的来指定行为与未定义的变量相关。o p c n m p 规范称某个交量为未定义的， 是摆该变爨鲍内容无毒效瓣建，或者该变蠡兹分酝或关联凌态无蠢效匏状态嘲。0 p e 心礤 程序中的变量成为未定义的条件可以分为两类，如裘2 2 所示。依赖于未定义的变量的未指 怠行为包揍对未定义变量鼓僵的使用和寝羧于未定义变量驰分配状态或关联状态翡操作。 表2 10 p e i l m p 规范中的未指定行为 类别未攫定行为举铡 个数 定义2 前使用由眦l l e l 确定的并行区中被该指导 蠡令赝带匏p 袋a i e 攒定的交爨 l a s 弧啊v a 聪指定的交蔗没有被其所在的d o 区的煅 与寒定义弱燮量程关聂一次迭煲或s 嚣c 曩o k s 逐豹最嚣一令删o n 赋篡， 1 3 且在这两个区之尉定义之前使用该变量 带慰溅t l 国戆绩撞怠食n o w a 疆，显在该结搀乏嚣 的第一个栅栏同步宪成之前使用规约变量 与数撰懿共享壤 耋摆关在w 。r x s 巍舡结搀审对程毒瓣挺量交餐戆赋选 l 与同步相关不占有锁的线程调用释放该镄的库例程 4 其它强及匈串的表达式调用包含副作用酌蕊数 2 本文称每类未指定行为在程序运行时的一次出现为该类未指定行为的一个实例。例 如，圈2 1 巾程序酌第7 行毽含第一爽未指定行为静一个实镄。由表2 2 知，p v 艚嚣指定的 变嫩k 在进入并行聪时是未定义的。着第4 彳予的控制条件取使为假，则在第7 行的语句使用k 之麓，k 渴米被定义。赉表2 1 知，这次交嚣使靥是奄未定义酌交蠹楣关的采指定行为豹一 个实例。朱指定行为不是程序员编程的真实意图，可能使稷序产生错误的计算结果或异常 结窳。该类行为是凌予程黟受对与寒据定季孑麓穗美熬o p c 删pa p l 误焉酝致。 第7 页 国防科学技术大学研究擞院学位论文 袭2 2o p e n m p 程序中的变缀未定义的条件 类裂变鬣来定义麴条搏举爨 个数 与数据的共享p a r a l l e l 所带的p r j v a t e 指定的变量在进入由该指导命令 1 0 鹱缝槎关确定的并霉区黠是未定义豹 若l a s l p 赳v a t e 指定的变量没有被其所在的d o 区的最后一次 迭我袋s e e 蕈l 溅s 区静鞭螽一个s e 傩 躐毽，剐在邃出这强 个区时该变量媳未定义的。 与瓣步穗关若带跹弱c 羊l 蹦簸訇静结构包禽n o w a l t 簸匈，猁篾约交爨 3 在该结构之后的第一个栅栏同步完成之前是采定义的 1 p m g r a md e m o l l le n dp r o g r a md e m 0 1 2f e a d4 。矗 31 $ o m p 触r a l l e lp 砒v a t e ( 的1 2s u b r o u t i 玎ew o 呔( m ) 4 i f ( a e q 1 o ) t h 黼 1 3r e a d + n 5k = 2 1 4 d o j = | ，n 6e i s e1 5 小= 煳+ ， 7j 邕詹 1 6e n d d o 8 魁通i fi 7掰= ：+ 嘏 9 c a l l w o r k 1 8 p r i n t ，m l o ! $ o 泔e n dp a r a l l e l1 9 ds u k 锄l 辆ew o 墩 图2 1 可能包含依赖于未定义交擞的未指定行为的实例的o p e i l m p 程序 2 2 岛栅栏阔步相关的死锁 死锁是指程序中的多个线程因飘相等待而陷入不能继续运行的德局。岛栅栏同步相关 煞廷镁是融蒯p 稷彦孛一炎鬻冤豹死镁。该类琵谈莛由予程序员谈屠b a 戳疆浆等弱步结 构所致。o p e l l m p a p i 中的b a r r i e r 指导命令指明了一个栅栏同步点。与b a 咖r 绑定的 并行嚣是惫会其豹簸蠹层戆舞孬嚣。鲰蘸傍静语义要求执行与b 矧醚e r 绨定戆势行送豹 线程组中的所有线程到达该同步点厨，这些线程才能继续执行该同步点之厝的代码。后文 奁分摄帮梭溅死锬懑缓设挠簿劳簿嚣懿线糕缝惫食豹线程瓣数器大予l 。 与栅栏同步相关的死锁可以分为两类。一类是b a u e r 紧嵌套于并行医中且仪被执行 该势孬区的线程缀孛的一令线程遇到；另一类是b 划蕊e r 紧嵌套予劳孬区孛基竣撬磐该势 彳亍麟的线稷组中的铸个线稷遇到的次数不完全相同。若一个区嵌套在另一个区之中，且没 有势行区嫩套在二瓣之间，则藏一令区被拣为紧嵌囊予后一个区之枣睇o l 。扶壤念上 ； ，第 二裘死锁包含了第一类死锁。本文之所以如此对与栅栏同步相关的死锁分类，是因为两类 死锁的检测方法不阉。存在性规则和非一致性规则分别被用于捡测第一类秘第二类死锬。 帮8 页 国防科举技术大学研究生院学位论文 与未指定行为类似，本文称每类死锁在程序运行时的一次鼢现为该粪死锁的一个实例。图 2 ，2 绘出了鼗个分别包含鼹炎死锬鲍实倒豹o p e 心哇p 程序。 l p r o g r a md e m 0 2 1 p r o g r a md e m 0 3 2s = 02 e 鑫珏零t j 嘲搀羚醚s ( 舄 3c a l lo m p _ s e l _ j u “l - t h r e a d s ( 4 )3 1 $ o 咿p a r a l i 正lp r j v a t e ( t i d ) 4l $ o 脚p a r a l l e lp r i v a t e ( 虹d )4 t i d = 0 m p 艘t n a 畦j l u l n o 5 髓= o m pg e t 粕- n u m o 5 i f 秘糙 4 ) t i ! 旧n 61 $ o 咿c r j t i c a l61 s o m pb a r n l e r 7s u m 邕s 聪拄+ l l 鑫7 e l s e 81 s o m pb a r r l e r 8 州n t + ，t i d 91 $ o 噼e n dc r t i c a l9尊n