基于Dixon结式和逐次差分代换的多项式秩函数探测方法
|
摘要
秩函数探测是循环程序终止性分析的重要方法,目前,已有很多研究者致力于为线性循环程序探测对应的线性秩函数,然而,针对具有多项式循环条件和多项式赋值的多项式型的循环,现有的秩函数探测方法还有所不足,解决方案大多是不完备的、或者具有较高的时间复杂度。针对现有工作对于多项式秩函数探测方法不足的问题,基于扩展Dixon结式(KSY方法)和逐次差分代换(SDS)方法,提出一种为多项式循环程序探测多项式型秩函数的方法。首先,将待探测的秩函数模板看作带参数系数的多项式,将秩函数的探测转换为寻找满足条件的参数系数的问题;然后,进一步将问题转换为判定相应的方程组是否有解的问题,至此,利用KSY方法中的扩展的Dixon结式,将问题更进一步简化为带参系数多项式(即结式)严格为正的判定问题;最后,利用SDS方法,找到一个充分条件,使得得到的结式严格为正,此时,可以获取满足条件的参数系数的取值,从而找到一个满足条件的秩函数,通过实验验证该秩函数探测方法的有效性。实验结果表明,利用该方法,可以有效地为多项式循环程序找到多项式秩函数,包括深度为d的多阶段多项式秩函数,与已有方法相比,该方法能够更高效地找到多项式秩函数,对于基于柱形代数分解(CAD)方法的探测方法因时间复杂度问题无法而应对的一些循环,利用所提方法能够在几秒内为这些循环找到秩函数。
Ranking function detection is one of the most important methods to analyze the termination of loop program. Some tools have been developed to detect linear ranking functions corresponding to linear loop programs. However, for polynomial loops with polynomial loop conditions and polynomial assignments, existing methods for detecting their ranking functions are mostly incomplete or with high time complexity. To deal with these weaknesses of existing work, a method was proposed for detecting polynomial ranking functions for polynomial loop programs, which was based on extended Dixon resultants(the KSY(Kapur-Saxena-Yang) method) and Successive Difference Substitution(SDS) method. Firstly, the ranking functions to be detected were seen as polynomials with parametric coefficients. Then the detection of ranking functions was transformed to the problem of finding parametric coefficients satisfying the conditions. Secondly, this problem was further transformed to the problem of determining whether the corresponding equations have solutions or not. Based on extended Dixon resultants in KSY method, the problem was reduced to the decision problem whether the polynomials with symbolic coefficients(resultants) were strictly positive or not. Thirdly, a sufficient condition making the resultants obtained strictly positive were found by SDS method. In this way, the coefficients satisfying the conditions were able to be obtained and thus a ranking function satisfying the conditions was found. The effectiveness of the method was proved by experiments. The experimental results show that polynomial ranking functions including d-depth multi-stage polynomial ranking functions are able to be detected for polynomial loop programs. This method is more efficient to find polynomial ranking functions compared with the existing methods. For loops whose ranking functions cannot be detected by the method based on Cylindrical Algebraic Decomposition(CAD) due to high time complexity, their ranking functions are able be found within a few seconds with the proposed method.
Ranking function detection is one of the most important methods to analyze the termination of loop program. Some tools have been developed to detect linear ranking functions corresponding to linear loop programs. However, for polynomial loops with polynomial loop conditions and polynomial assignments, existing methods for detecting their ranking functions are mostly incomplete or with high time complexity. To deal with these weaknesses of existing work, a method was proposed for detecting polynomial ranking functions for polynomial loop programs, which was based on extended Dixon resultants(the KSY(Kapur-Saxena-Yang) method) and Successive Difference Substitution(SDS) method. Firstly, the ranking functions to be detected were seen as polynomials with parametric coefficients. Then the detection of ranking functions was transformed to the problem of finding parametric coefficients satisfying the conditions. Secondly, this problem was further transformed to the problem of determining whether the corresponding equations have solutions or not. Based on extended Dixon resultants in KSY method, the problem was reduced to the decision problem whether the polynomials with symbolic coefficients(resultants) were strictly positive or not. Thirdly, a sufficient condition making the resultants obtained strictly positive were found by SDS method. In this way, the coefficients satisfying the conditions were able to be obtained and thus a ranking function satisfying the conditions was found. The effectiveness of the method was proved by experiments. The experimental results show that polynomial ranking functions including d-depth multi-stage polynomial ranking functions are able to be detected for polynomial loop programs. This method is more efficient to find polynomial ranking functions compared with the existing methods. For loops whose ranking functions cannot be detected by the method based on Cylindrical Algebraic Decomposition(CAD) due to high time complexity, their ranking functions are able be found within a few seconds with the proposed method.
引文
[1] LEIKE J,HEIZMANN M.Geometric nontermination arguments [C]// TACAS 2018:Proceedings of the 2018 International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2018:172-186.
[2] FEDYUKOVICH G,ZHANG Y L,GUPTA A.Syntax-guided termination analysis[C]// CAV 2018:Proceedings of the 2018 International Conference on Computer Aided Verification.Berlin:Springer,2018:124-143.
[3] CHEN Y F,HEIZMANN M,LENGAL O,et al.Advanced automata-based algorithms for program termination checking[C]// PLDI 2018:Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation.New York:ACM,2018:135-150.
[4] LI Y.Witness to non-termination of linear programs[J].Theoretical Computer Science,2017,681:75-100.
[5] CHEN Y H,XIA B C,YANG L,et al.Discovering non-linear ranking functions by solving semi-algebraic systems[C]// ICTAC 2007:Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing.Berlin:Springer,2007:34-49.
[6] COLON M,SPIMA H.Synthesis of linear ranking functions[C]// TACAS 2001:Proceedings of the 2001 International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2001:67-81.
[7] COLON M,SPIMA H.Practical methods for proving program termination[C]// CAV 2002:Proceedings of the 2002 International Conference on Computer Aided Verification.Berlin:Springer,2002:442-454.
[8] PODELSKI A,RYBALCHENKO A.A complete method for the synthesis of linear ranking functions[C]// VMCAI 2004:Proceedings of the 2004 International Conference on Verification,Model Checking and Abstract Interpretation.Berlin:Springer,2004:239-251.
[9] SCHRIJVER A.Theory of Linear and Integer Programming [M].New York:John Wiley and Sons,Inc.,1986:87-90.
[10] BEN-AMRAM A M,GENAIM S.Ranking functions for linear-constraint loops[J].Journal of the ACM,2014,61(4):Article No.26.
[11] TURING A M.On computable numbers,with an application to the entscheidungs problem[J].Proceedings of the London Mathematical Society,1937,42(2):230-265.
[12] BRAVEMAN M.Termination of integer linear programs[C]// CAV 2006:Proceedings of the 2006 International Conference on Computer Aided Verification.Berlin:Springer,2006:372-385.
[13] TIWARI A.Termination of linear programs[C]// CAV 2004:Proceedings of the 2004 International Conference on Computer Aided Verification.Berlin:Springer,2004:70-82.
[14] YANG L,ZHAN N J,XIA B C,et al.Program verification by using DISCOVERER[C]// VSTTE 2005:Proceedings of the 2005 Working Conference on Verified Software:Theories,Tools,and Experiments.Berlin:Springer,2008:528-538.
[15] BAGNARA R,MESNARD F.Eventual linear ranking functions[C]// PPDP 2013:Proceedings of the 2013 International Symposium on Principles and Practice of Declarative Programming.New York:ACM,2013:229-238.
[16] BEN-AMRAM A M,GENAIM S.On multiphase-linear ranking functions[C]// CAV 2017:Proceedings of the 2017 International Conference on Computer Aided Verification.Berlin:Springer,2017:601-620.
[17] BRADLEY A R,MANNA Z,SIPMA H B.Linear ranking with reachability[C]// CAV 2005:Proceedings of the 2005 International Conference on Computer Aided Verification.Berlin:Springer,2005:491-504.
[18] BRADLEY A R,MANNA Z,SIPMA H B.The polyranking principle[C]// ICALP 2005:Proceedings of the 2005 International Conference on Automata,Languages and Programming.Berlin:Springer,2005:1349-1361.
[19] LEIKE J,HEIZMANN M.Ranking templates for linear loops[C]// TACAS 2014:Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2014:172-186.
[20] LI Y,ZHU G,FENG Y.The L-depth eventual linear ranking functions for single-path linear constraint loops[C]// TASE 2016:Proceedings of the 2016 International Symposium on Theoretical Aspects of Software Engineering.Piscataway,NJ:IEEE,2016:30-37.
[21] COUSOT P.Proving program invariance and termination by parametric abstraction,Lagrangian relaxation and semidefinite programming[C]// VMCAI 2005:Proceedings of the 2005 International Conference on Verification,Model Checking and Abstract Interpretation.Berlin:Springer,2005:1-24.
[22] SHEN L Y,WU M,YANG Z F,et al.Generating exact nonlinear ranking functions by symbolic-numeric hybrid method[J].Journal of Systems Science and Complexity,2013,26(2):291-301.
[23] KAPUR D,SAXENA T,YANG L.Algebraic and geometric reasoning using Dixon resultants[C]// ISSAC 1994:Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation.New York:ACM,1994:99-107.
[24] YANG L.Solving harder problems with lesser mathematics[C]// ATCM 2005:Proceedings of the 2005 Asian Technology Conference in Mathematics.Radford,VA:Mathematics and Technology,2005:37-46.
[25] DIXON A L.The eliminant of three quantics in two independent variables[J].Proceedings of the London Mathematical Society,1909,s2- 7(49):49-69.
[26] 杨路,姚勇.差分代换矩阵与多项式的非负性判定[J].系统科学与数学,2009,29(9):1169-1177.(YANG L,YAO Y.Difference substitution matrices and decision on nonnegativity of polynomials [J].Journal of Systems Science and Mathematical Sciences,2009,29(9):1169-1177.)
[27] HOU X R,SHAO J W.Bounds on the number of steps of WDS required for checking the positivity of integral forms[J].Applied Mathematics and Computation,2011,217(24):9978-9984.
[28] 韩京俊.基于差分代换的正半定型判定完备方法[J].北京大学学报(自然科学版),2013,49(4):545-551.(HAN J J.A complete method based on successive difference substitution method for deciding positive semi-definiteness of polynomials[J].Acta Scientiarum Naturalium Universitatis Pekinensis,2013,49(4):545-551.)
[29] 杨路.差分代换与不等式机器证明[J].广州大学学报(自然科学版),2006,5(2):1-7.(YANG L.Difference substitution and automated inequality proving[J].Journal of Guangzhou University (Natural Science edition),2006,5(2):1-7.)
[30] QIN X,WU D,TANG L,et al.Complexity of constructing Dixon resultant matrix[J].International Journal of Computer Mathematics,2016,94(10):1-16.
[31] LI Y.An effective hybrid algorithm for computing symbolic determinants[J].Applied Mathematics and Computation,2009,215(7):2495-2501.
[32] KALTOFEN E.On computing determinants of matrices without divisions [C]// ISSAC 1992:Proceedings of the 1992 International Symposium on Symbolic and Algebraic Computation.New York:ACM,1992:342-349.
[2] FEDYUKOVICH G,ZHANG Y L,GUPTA A.Syntax-guided termination analysis[C]// CAV 2018:Proceedings of the 2018 International Conference on Computer Aided Verification.Berlin:Springer,2018:124-143.
[3] CHEN Y F,HEIZMANN M,LENGAL O,et al.Advanced automata-based algorithms for program termination checking[C]// PLDI 2018:Proceedings of the 2018 ACM SIGPLAN Conference on Programming Language Design and Implementation.New York:ACM,2018:135-150.
[4] LI Y.Witness to non-termination of linear programs[J].Theoretical Computer Science,2017,681:75-100.
[5] CHEN Y H,XIA B C,YANG L,et al.Discovering non-linear ranking functions by solving semi-algebraic systems[C]// ICTAC 2007:Proceedings of the 2007 International Colloquium on Theoretical Aspects of Computing.Berlin:Springer,2007:34-49.
[6] COLON M,SPIMA H.Synthesis of linear ranking functions[C]// TACAS 2001:Proceedings of the 2001 International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2001:67-81.
[7] COLON M,SPIMA H.Practical methods for proving program termination[C]// CAV 2002:Proceedings of the 2002 International Conference on Computer Aided Verification.Berlin:Springer,2002:442-454.
[8] PODELSKI A,RYBALCHENKO A.A complete method for the synthesis of linear ranking functions[C]// VMCAI 2004:Proceedings of the 2004 International Conference on Verification,Model Checking and Abstract Interpretation.Berlin:Springer,2004:239-251.
[9] SCHRIJVER A.Theory of Linear and Integer Programming [M].New York:John Wiley and Sons,Inc.,1986:87-90.
[10] BEN-AMRAM A M,GENAIM S.Ranking functions for linear-constraint loops[J].Journal of the ACM,2014,61(4):Article No.26.
[11] TURING A M.On computable numbers,with an application to the entscheidungs problem[J].Proceedings of the London Mathematical Society,1937,42(2):230-265.
[12] BRAVEMAN M.Termination of integer linear programs[C]// CAV 2006:Proceedings of the 2006 International Conference on Computer Aided Verification.Berlin:Springer,2006:372-385.
[13] TIWARI A.Termination of linear programs[C]// CAV 2004:Proceedings of the 2004 International Conference on Computer Aided Verification.Berlin:Springer,2004:70-82.
[14] YANG L,ZHAN N J,XIA B C,et al.Program verification by using DISCOVERER[C]// VSTTE 2005:Proceedings of the 2005 Working Conference on Verified Software:Theories,Tools,and Experiments.Berlin:Springer,2008:528-538.
[15] BAGNARA R,MESNARD F.Eventual linear ranking functions[C]// PPDP 2013:Proceedings of the 2013 International Symposium on Principles and Practice of Declarative Programming.New York:ACM,2013:229-238.
[16] BEN-AMRAM A M,GENAIM S.On multiphase-linear ranking functions[C]// CAV 2017:Proceedings of the 2017 International Conference on Computer Aided Verification.Berlin:Springer,2017:601-620.
[17] BRADLEY A R,MANNA Z,SIPMA H B.Linear ranking with reachability[C]// CAV 2005:Proceedings of the 2005 International Conference on Computer Aided Verification.Berlin:Springer,2005:491-504.
[18] BRADLEY A R,MANNA Z,SIPMA H B.The polyranking principle[C]// ICALP 2005:Proceedings of the 2005 International Conference on Automata,Languages and Programming.Berlin:Springer,2005:1349-1361.
[19] LEIKE J,HEIZMANN M.Ranking templates for linear loops[C]// TACAS 2014:Proceedings of the 2014 International Conference on Tools and Algorithms for the Construction and Analysis of Systems.Berlin:Springer,2014:172-186.
[20] LI Y,ZHU G,FENG Y.The L-depth eventual linear ranking functions for single-path linear constraint loops[C]// TASE 2016:Proceedings of the 2016 International Symposium on Theoretical Aspects of Software Engineering.Piscataway,NJ:IEEE,2016:30-37.
[21] COUSOT P.Proving program invariance and termination by parametric abstraction,Lagrangian relaxation and semidefinite programming[C]// VMCAI 2005:Proceedings of the 2005 International Conference on Verification,Model Checking and Abstract Interpretation.Berlin:Springer,2005:1-24.
[22] SHEN L Y,WU M,YANG Z F,et al.Generating exact nonlinear ranking functions by symbolic-numeric hybrid method[J].Journal of Systems Science and Complexity,2013,26(2):291-301.
[23] KAPUR D,SAXENA T,YANG L.Algebraic and geometric reasoning using Dixon resultants[C]// ISSAC 1994:Proceedings of the 1994 International Symposium on Symbolic and Algebraic Computation.New York:ACM,1994:99-107.
[24] YANG L.Solving harder problems with lesser mathematics[C]// ATCM 2005:Proceedings of the 2005 Asian Technology Conference in Mathematics.Radford,VA:Mathematics and Technology,2005:37-46.
[25] DIXON A L.The eliminant of three quantics in two independent variables[J].Proceedings of the London Mathematical Society,1909,s2- 7(49):49-69.
[26] 杨路,姚勇.差分代换矩阵与多项式的非负性判定[J].系统科学与数学,2009,29(9):1169-1177.(YANG L,YAO Y.Difference substitution matrices and decision on nonnegativity of polynomials [J].Journal of Systems Science and Mathematical Sciences,2009,29(9):1169-1177.)
[27] HOU X R,SHAO J W.Bounds on the number of steps of WDS required for checking the positivity of integral forms[J].Applied Mathematics and Computation,2011,217(24):9978-9984.
[28] 韩京俊.基于差分代换的正半定型判定完备方法[J].北京大学学报(自然科学版),2013,49(4):545-551.(HAN J J.A complete method based on successive difference substitution method for deciding positive semi-definiteness of polynomials[J].Acta Scientiarum Naturalium Universitatis Pekinensis,2013,49(4):545-551.)
[29] 杨路.差分代换与不等式机器证明[J].广州大学学报(自然科学版),2006,5(2):1-7.(YANG L.Difference substitution and automated inequality proving[J].Journal of Guangzhou University (Natural Science edition),2006,5(2):1-7.)
[30] QIN X,WU D,TANG L,et al.Complexity of constructing Dixon resultant matrix[J].International Journal of Computer Mathematics,2016,94(10):1-16.
[31] LI Y.An effective hybrid algorithm for computing symbolic determinants[J].Applied Mathematics and Computation,2009,215(7):2495-2501.
[32] KALTOFEN E.On computing determinants of matrices without divisions [C]// ISSAC 1992:Proceedings of the 1992 International Symposium on Symbolic and Algebraic Computation.New York:ACM,1992:342-349.