欢迎来到麦多课文档分享! | 帮助中心 海量文档,免费浏览,给你所需,享你所想!
麦多课文档分享
全部分类
  • 标准规范>
  • 教学课件>
  • 考试资料>
  • 办公文档>
  • 学术论文>
  • 行业资料>
  • 易语言源码>
  • ImageVerifierCode 换一换
    首页 麦多课文档分享 > 资源分类 > PPT文档下载
    分享到微信 分享到微博 分享到QQ空间

    Automatic Synthesis of Fault-Tolerance.ppt

    • 资源ID:378750       资源大小:153.50KB        全文页数:43页
    • 资源格式: PPT        下载积分:2000积分
    快捷下载 游客一键下载
    账号登录下载
    微信登录下载
    二维码
    微信扫一扫登录
    下载资源需要2000积分(如需开发票,请勿充值!)
    邮箱/手机:
    温馨提示:
    如需开发票,请勿充值!快捷下载时,用户名和密码都是您填写的邮箱或者手机号,方便查询和重复下载(系统自动生成)。
    如需开发票,请勿充值!如填写123,账号就是123,密码也是123。
    支付方式: 支付宝扫码支付    微信扫码支付   
    验证码:   换一换

    加入VIP,交流精品资源
     
    账号:
    密码:
    验证码:   换一换
      忘记密码?
        
    友情提示
    2、PDF文件下载后,可能会被浏览器默认打开,此种情况可以点击浏览器菜单,保存网页到桌面,就可以正常下载了。
    3、本站不支持迅雷下载,请使用电脑自带的IE浏览器,或者360浏览器、谷歌浏览器下载即可。
    4、本站资源下载后的文档和图纸-无水印,预览文档经过压缩,下载后原文更清晰。
    5、试题试卷类文档,如果标题没有明确说明有答案则都视为没有答案,请知晓。

    Automatic Synthesis of Fault-Tolerance.ppt

    1、Automatic Synthesis of Fault-Tolerance,Ali Ebnenasir Software Engineering and Network Systems Laboratory Computer Science and Engineering Department Michigan State UniversityAdvisor: Dr. Sandeep Kulkarni,2,Problem,Given a program p and a class of faults f,Question: How do we add desired fault-tolera

    2、nce properties to p in order to create a new program p such that:Requirements:In the absence of f, the resulting fault-tolerant program p behaves similar to p In the presence of f, the resulting fault-tolerant program p satisfies the desired fault-tolerance property.,3,Solution Strategies,Two possib

    3、le approachesRedesign p and verify its correctness w.r.t problem requirements Expensive approachAutomatically synthesize p from p Correct by construction,4,Previous Work on Automated Synthesis,5,Synthesis: Specification-Based,Specification of p (Temporal Logic Expressions/ Automata),Synthesis Algori

    4、thm (prove the satisfiabilityof the specification),Faults,Fault-tolerancerequirements (Temporal Logic Expressions),Fault-tolerant program p,Program synthesis: Fault-Tolerance synthesis:EmersonClarke 1982 AroraAttieEmerson 1998 AttieEmerson 2001 KupfermannVardi 2001,6,Synthesis: Calculational,Kulkarn

    5、iArora 2000 KulkarniAroraChippada 2001,Fault-intolerant program p (Transitions),Synthesis Algorithm (Calculate the set of transitions),Fault-tolerant program p (Transitions),Fault-tolerance requirements,Faults (Transitions),7,The Complexity of Calculational Synthesis,High atomicity model: processes

    6、can atomically read/write all program variables Polynomial in the state space of the fault-intolerant program p KA00Low atomicity model (distributed programs): processes have read/write restrictions with respect to program variablesExponential in the state space of the fault-intolerant program p for

    7、 synthesizing masking fault-tolerance KA00,KA00 S.S. Kulkarni and A. Arora, Automating the addition of fault-tolerance, FTRTFT 2000.,Propose techniques for the synthesis of fault-tolerant distributed programs,8,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues Step-wi

    8、se automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,9,Preliminary Concepts: Programs and Faults,Program Finite number of variables with finite domains Finite

    9、 number of processes State: a valuation of program variables Finite state space Sp State predicate X X Sp Program p, Fault f (s0, s1) | (s0, s1) Sp Sp Closure: X is closed in p,Sp,10,Preliminary Concepts: Specifications and Fault-Tolerance,Safety specification: something bad never happens Representa

    10、tion (s0, s1) | (s0, s1) Sp Sp E.g., transitions that change the value of a counter from non-zero values to zero Liveness specification: something good will eventually happen In the absence of faults, fault-tolerant program p satisfies the liveness specification of the fault-intolerant program p Inv

    11、ariant S, fault-span T Sp Fault-tolerance: Failsafe, Nonmasking, Masking,Sp,Program,Fault,11,Preliminary Concepts: Distribution Model,Read/Write restrictions (low atomicity model) Assumption: a process cannot write a variable that it cannot read. Example: program p Two processes j, k Two Boolean var

    12、iables a and b Process j cannot read b, but can read and write a Write restrictions Can we include the following transition in the set of transitions of process j?,Write restrictions identify the set of transitions of each process.,j,k,a,b,12,Preliminary Concepts: Distribution Model Continued,Read r

    13、estrictions Can we include the following transition in the set of transitions of process j?,Groups of transitions (instead of individual transitions) must be chosen.,13,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues Step-wise automation Polynomial-time boundary Heu

    14、ristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,14,Synthesis Problem,Synthesis Algorithm,Fault-intolerantprogram p,Specification Spec,Invariant S,(Masking/Nonmasking/Failsafe)Fault-tolerantprogra

    15、m p,Invariant S,Faults f,Distribution restrictions,Requirements No new behaviors are added in the absence of faults. In the presence of faults, p provides desired level of fault-tolerance.,Desired level of Fault-intolerance(Masking/Nonmasking/Failsafe),15,Outline,Preliminary concepts Synthesis probl

    16、em Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,16,Theoretical Issues: Step-Wise Automation,Intolerant Progr

    17、am,Masking fault-tolerant,Failsafe,KA00,17,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs C

    18、ontributions Open problems,18,Theoretical Issues: Polynomial-Time Boundary,Complexity: reduction from 3-SAT to the problem of synthesizing failsafe fault-tolerant distributed programs In general, the problem of synthesizing failsafe fault-tolerant distributed programs from their fault-intolerant ver

    19、sion is NP-complete. Intuitively, the exponential complexity is due to the inability of a process to safely estimate unreadable variables even in the absence of faults (grouping issue).What are the necessary and sufficient conditions for polynomial synthesis of failsafe fault-tolerant distributed pr

    20、ograms? Restrictions on The transitions of the fault-intolerant programs Specifications,19,Theoretical Issues: Monotonicity of Specifications,Definition: A specification spec is positive monotonic with respect to a Boolean variable x iff: For every (s0, s1) and (s0, s1) grouped together due to inabi

    21、lity of reading x,20,Theoretical Issues: Monotonicity of Programs,Definition: Program p with invariant S is positive monotonic with respect to a Boolean variable x iff: For every (s0, s1) and (s0, s1) grouped together due to inability of reading x,Monotonicity requirements capture the notion that sa

    22、fe assumptions can be made about variables that cannot be read,21,Theoretical Issues: Monotonicity Theorem,Sufficiency: if Program is negative monotonic, and Spec is positive monotonic Or Program is positive monotonic, and Spec is negative monotonic Then Synthesis of failsafe fault-tolerance can be

    23、done in polynomial time Necessity: If only one of these conditions is satisfied then synthesizing failsafe fault-tolerance remains NP-complete. For many problems, these requirements are easily met (e.g., Byzantine agreement, consensus, atomic commit),22,Theoretical Issues: An Example for Monotonicit

    24、y Theorem,Dijkstras guarded commands (actions) Guard Statement (s0, s1) | Guard holds at s0 and atomic execution of Statement yields s1 Example: Byzantine agreement Safety Specification of Byzantine agreement:Agreement: No two non-Byzantine non-generals can finalize with different decisions Validity

    25、: If g is not Byzantine then no non-Byzantine process can finalize with a different decision with respect to gProcesses: General, g, and three non-generals j, k, and l d.g : 0, 1 d.j, d.k, d.l : 0, 1, b.g, b.j, b.k, b.l : 0, 1 f.j, f.k, f.l : 0, 1,g,l,k,j,23,Theoretical Issues: An Example for Monoto

    26、nicity Theorem,Program actions for process j d.j = f.j = 0 d.j := d.g d.j f.j = 0 f.j := 1Fault transitions for process j b.g b.j b.k b.l b.j := 1 b.j d.j :=0|1Read/Write restrictions: Readable variables for process j: b.j, d.j, f.j, d.g, d.k, d.l Process j can write d.j, f.j,24,Theoretical Issues:

    27、An Example for Monotonicity Theorem Continued,Observation 1: Negative monotonicity of specification with respect to f.j Observation 2: Positive monotonicity of program, consisting of the transitions of j, with respect to f.kObservation 3: Positive monotonicity of specification with respect to b.j Th

    28、e specification does not stipulate anything about the Byzantine processes Observation 4: Negative monotonicity of program, consisting of the transitions of j, with respect to b.k,Synthesis of agreement program that is failsafe to Byzantine faults can be done in polynomial time.,25,Outline,Preliminar

    29、y concepts Synthesis problem Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,26,Theoretical Issues: Heuristics,

    30、Heuristic: A strategy for making deterministic decisions to reduce the complexity of synthesis Example: Reuse the structure of nonmasking programs in the synthesis of their masking versions,Intolerant Program,Masking fault-tolerant,Fault-Tolerance Enhancement,27,Outline,Preliminary concepts Synthesi

    31、s problem Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,28,Theoretical Issues: Pre-Synthesized Fault-Toleranc

    32、e Components,What if existing heuristics fail?How can we reuse the techniques used in the synthesis of a program, in the synthesis of another program?Can we encapsulate commonly encountered synthesis patterns in terms of pre-synthesized fault-tolerance components?Detectors and correctors are necessa

    33、ry and sufficient in the design of fault-tolerance AK98 Detectors and correctors have the potential to provide a rich library of pre-synthesized fault-tolerance components,AK98 A. Arora and S.S. Kulkarni, Detectors and Correctors: A Theory of Fault-Tolerance , IEEE ICDCS 1998.,29,Theoretical Issues:

    34、 Using Pre-Synthesized Components,If available heuristics fail to add recovery from a deadlock state sd,Automatically specify the required component,Extract the component from the component library,Verify the interference-freedom of the composition,Add extracted component to the fault-intolerant pro

    35、gram,30,Theoretical Issues: Pre-Synthesized Components - Achievements,Reducing the chance of failure in the synthesisProviding a mechanism for the reuse of synthesis techniques Extending the scope of synthesis problem where the state space is expanded during the synthesisControlling the way new vari

    36、ables are introduced,31,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open p

    37、roblems,32,Practical Issues: Framework Goals,Goals of the framework designAbility to synthesize fault-tolerant programs from their fault-intolerant versionsAbility to integrate new heuristics into the frameworkAbility to change implementation,33,Practical Issues: Synthesis Framework,Synthesis algori

    38、thm,Interactive user interface,The user (Fault-tolerance developer),Query,Query,Results,Results,p, S, f, spec,p, S, f, spec,p, S,p, S,Guarded commands, State predicates,Guarded commands/ Promela, State predicates,Library of pre-synthesized fault-tolerance components,Pre-synthesized detectors/correct

    39、ors,Component specification,34,Practical Issues: Framework Internals Synthesis Algorithm,Remove bad transitions,Remove bad states,Expand the reachability graph,Initialization,Ensure safety,Ensure deadlock freedom,Calculate a validfault-span,Preserve Invariant,Ensure deadlock freedom,Calculate a vali

    40、dinvariant,Modify Invariant,Resolve non-progress cycles,Reachability graph of the fault-tolerant program,Interaction points,p, S, f, spec,p, S,Fault-tolerant program,Fault-intolerant program,35,Practical Issues: Current Status of the Framework,Example synthesized programs: Token ring with 7 processe

    41、s Byzantine agreement with 4 non-general processes and one general process An agreement program that is subject to both Byzantine and fail-stop faults (1.3 million states)Currently, the framework can handle different types of faults (e.g., process restart, Byzantine, fail-stop) synthesize programs t

    42、hat are simultaneously subject to multiple types of faults,36,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues step-wise automation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-

    43、tolerant programs Contributions Open problems,37,Contributions,Showing the NP-completeness of synthesizing failsafe fault-tolerance Identifying the necessary and sufficient conditions for polynomial-time synthesis of failsafe fault-tolerance Reusing the computational structure of fault-intolerant pr

    44、ograms to reduce the complexity of synthesis (enhancement)Identifying synthesis patterns as pre-synthesized fault-tolerance components Developing a framework for the synthesis of fault-tolerant programs,38,Outline,Preliminary concepts Synthesis problem Current results Theoretical issues step-wise au

    45、tomation Polynomial-time boundary Heuristics Pre-synthesized fault-tolerance components Practical issues A framework for the synthesis of fault-tolerant programs Contributions Open problems,39,Open Problems,Theoretical issues Non-monotonic programs/specifications to monotonic ones Extending the scop

    46、e of the programs that can reap the benefit of efficient automation Necessary and sufficient conditions for simultaneous addition of multiple pre-synthesized fault-tolerance components Necessary and sufficient conditions for polynomial-time synthesis of nonmasking fault-tolerant programs Automated s

    47、ynthesis of multitolerance,40,Open Problems - Continued,Practical issues Distributed synthesis algorithm Symbolic synthesis of fault-tolerance,Distributed Synthesis Algorithm,SAT solver,SAT solver,Verify safety,Y/N,Closure,Y/N,Cycle detection,Y/N,. . .,SAT solver,41,Open Problems - Continued,Using m

    48、odel checkers for acquiring behavioral information during synthesis,Distributed Synthesis Algorithm,. . .,SPIN,SPIN,SPIN,42,Publications,Published papers Sandeep S. Kulkarni and Ali Ebnenasir. “Enhancing The Fault- Tolerance of Nonmasking Programs“. IEEE ICDCS 2003. Ali Ebnenasir. “Algorithmic Synth

    49、esis of Fault-Tolerant Distributed Programs“. Doctoral Symposium of ICDCS 2003. Sandeep S. Kulkarni and Ali Ebnenasir. “The Complexity of Adding Failsafe Fault-Tolerance“. IEEE ICDCS 2002. Submitted papers Sandeep S. Kulkarni and Ali Ebnenasir. “Adding Fault-Tolerance Using Pre-Synthesized Components“. Submitted to CBSE7, ICSE 2004. Ali Ebnenasir and Sandeep S. Kulkarni . “A Framework for Automatic Synthesis of Fault-Tolerance“. Submitted to DSN 2004. Sandeep S. Kulkarni and Ali Ebnenasir. “Automated Synthesis of Multitolerance“. Submitted to DSN 2004.,


    注意事项

    本文(Automatic Synthesis of Fault-Tolerance.ppt)为本站会员(deputyduring120)主动上传,麦多课文档分享仅提供信息存储空间,仅对用户上传内容的表现方式做保护处理,对上载内容本身不做任何修改或编辑。 若此文所含内容侵犯了您的版权或隐私,请立即通知麦多课文档分享(点击联系客服),我们立即给予删除!




    关于我们 - 网站声明 - 网站地图 - 资源地图 - 友情链接 - 网站客服 - 联系我们

    copyright@ 2008-2019 麦多课文库(www.mydoc123.com)网站版权所有
    备案/许可证编号:苏ICP备17064731号-1 

    收起
    展开