TLA+(参考https://lamport.azurewebsites.net/tla/learning.html)是Lamport大神发明的一种通过数学语言描述系统行为的工具。通过它,可以对系统的行为或者算法进行抽象描述,让系统或算法的开发人员或者想要了解系统或算法逻辑的第三方,可以忽略代码层级的细节,从更高层级的抽象逻辑上进行理解。TLA+语言描述的系统行为,不是静态的逻辑描述,而是可执行的代码,我们可以通过执行代码,模拟系统运行,从而观察系统运行的各个状态。同时,TLA+还提供了一整套的工具,可以校验、执行、debug TLA+代码。
本文尝试用TLA+来验证项目中遇到的实际问题,说明TLA+可以如何帮助开发人员写出正确的代码逻辑,并且帮助第三方理解。
问题描述
应用A要新增一种处理关联业务的场景,假设B1和B2是两种关联的业务,B1和B2请求有先后关系,上游系统会先给A发送一个B1请求,A回复处理成功,上游系统收到B1的结果之后再给A发送关联的B2请求,B1和B2请求通过一个linkId字段进行关联。当A系统没有开启蓄洪时,正常的处理流程是上游系统发起B1请求,A处理B1请求并回复处理成功,然后上游系统再发起B2请求,A再继续处理。当A系统开启蓄洪时,情况稍微复杂一点,这时A系统会先把请求保存下来,然后直接回复成功,再进行异步处理。业务上对B1和B2的实际处理顺序有要求,不管是否蓄洪,都要求必须B1处理完之后再处理B2。
问题分析
当A系统没有开启蓄洪时,上游系统先发起B1请求,处理完之后再发起B2请求,时序问题有保障;重点需要关注当A系统开启蓄洪时的场景。
未开启蓄洪时,请求受理过后先落库,落库时状态是INIT,然后进行预处理,预处理完状态变成ACCEPTED,然后进行异步处理,状态变成PROCESSING,处理成功之后,状态变成SUCCESS,处理失败则变成FAIL。整个状态变迁是由定时任务重试来保障成功的。
当开启蓄洪以后,请求受理过后先落库,落库时状态是INIT,然后进行预处理,预处理完状态变成FLOODING。当开始泄洪时,会批量将蓄洪状态的请求改成DISCHARGING,然后由定时任务捞取进行异步处理,状态变成PROCESSING,处理成功之后,状态变成SUCCESS,处理失败则变成FAIL。
如果系统A开启蓄洪,此时收到B1的请求,A直接回复成功,然后收到B2请求。这时B1、B2的请求都会被蓄洪,当泄洪时,由于B1和B2是异步处理,如果不做控制,B1和B2处理的顺序无法得到保障。为了满足B1和B2处理时序的要求,可以在B2处理时,判断一下关联的B1请求是否已处理完成,处理完就继续处理,否则就抛出异常,然后等待定时任务重试,最终等B1处理完之后,B2就可以处理。这个方案实现简单,但性能确很差,因为会有大量的重试请求,浪费处理资源。另一种方案是增加一个WAIT状态,表示当前交易不能处理,必须等待关联交易处理完之后才能处理,定时任务捞取执行时,会忽略WAIT状态的请求。当B2请求受理时,检查相应的B1请求是否已处理成功,如果是,则根据当前是否已开启蓄洪开关,将B2的状态改为FLOODING或者ACCEPTED;如果否,则将B2状态改成WAIT状态,当关联的B1请求处理完之后,则将关联的B2请求的状态从WAIT改成FLOODING或者ACCEPTED,这样等到下次定时任务将B2捞取时,就可以顺利执行。
算法描述
以下采用类Java的伪代码描述算法过程,主要用途是描述思路。
数据结构
这里定义数据结构中的关键字段,省略了和算法思路无关的细节。
BizReq定义了业务请求的关键字段
//业务请求classBizReq{//请求唯一标识StringbizNo;//关联idStringlinkId;//交易阶段,取值:B1, B2Stringphase;//状态,取值:null,INIT,ACCEPTED,PROCESSING,WAIT,FLOODING,DISCHARGING,SUCCESS,FAILStringstatus; }其中phase是表示该请求是B1场景的请求还是B2场景的请求。status表示请求的状态,算法中通过修改状态来模拟实际的业务处理过程。
SysStatus用来控制系统的全局状态,其中enableFlooding表示是否开启蓄洪,默认为false;enableDischarging表示是否开启泄洪,默认false。
//系统状态classSysStatus{//是否开启蓄洪staticbooleanenableFlooding;//是否开启泄洪staticbooleanenableDischarging; }请求受理
//查找关联的另一笔请求BizReqfindRelatedReq(BizReq req){ }voidsaveRequest(BizReq req){ req.status ="INIT";//save和其他操作}//受理请求voidacceptRequest(BizReq req){if(!req.status.equals("INIT")) {return; }if(SysStatus.enableFlooding) {if(req.phase.equals("B1")) { req.status ="FLOODING"}else{ BizReq b1Req = findRelatedReq(req);if(another ==null) { req.status ="WAIT";return; }if(b1.status.equals("SUCCESS")) { req.status ="FLOODING"}else{ req.status ="WAIT"; } } }else{if(req.phase.equals("B1")) { req.status ="ACCEPTED"; }else{ BizReq b1Req = findRelatedReq(req);if(another ==null) { req.status ="WAIT";return; }if(b1.status.equals("SUCCESS")) { req.status ="ACCEPTED"}else{ req.status ="WAIT"; } } } }异步处理及通知
异步处理由定时任务从数据库捞取出来执行,执行完结果,由下游回调应用A通知结果。
//异步处理请求voidprocessReq(BizReq req){if(req.status.equals("ACCEPTED") || req.status.equals("DISCHARGING")) { req.status ="PROCESSING"; } }//异步处理结果通知。如果抛出NeedRetryException,则表示需要调用方稍后重试voidnotifyResult(BizReq req){if(req.phase.equals("B1")) {if(req.status.equals("SUCCESS")) { BizReq b2Req = findRelatedReq(req);if(b2Req ==null) {return; }if(b2Req.status.equals("INIT")) {thrownewNeedRetryException(); }if(b2Req.status.equals("WAIT")) {if(SysStatus.enableFlooding) { b2Req.status ="FLOODING"; }else{ b2Req.status ="ACCEPTED"; } } } } }泄洪
泄洪时,由定时任务捞取蓄洪状态的请求,修改其状态,然后由异步执行定时任务去执行。这里忽略定时任务处理的部分,只关注状态修改。
voiddischarging(BizReq req){ req.status ="DISCHARGING"; }算法验证
上述算法过程只关注状态变迁,而省略了具体的业务处理逻辑,以及定时任务处理细节,以及异常处理等。即便如此,由于上述算法的状态机本身比较复杂,而且涉及多线程状态修改,上述算法的正确性难以保障。按照传统的思路,要想验证上述算法的正确性,只能将上述算法逻辑实现出来,然后列举所有可能的场景,手动验证每一种场景的处理结果是否符合预期。这样的做法有以下几个问题:
实现过后再验证,验证的时间点比较靠后,无法直接验证算法逻辑本身的完备性靠手动列举场景的方式验证,工作量大,而且容易遗漏,而且对测试人员的素质要求很高,必须具备很强的逻辑思维能力由于是分布式系统,如果测试发现问题,debug过程比较繁琐因此,这里准备采用TLA+,先验证算法本身的正确性和完备性,算法逻辑验证通过之后,再去写代码,就更不容易出错。
TLA+代码
---------------------------- MODULE LinkedOrder ---------------------------- EXTENDS Integers, FiniteSets * system status VARIABLES enableFlooding, enableDischaring * transactions status VARIABLES b1Req, b2Req INIT == / b1Req =""/ b2Req =""/ enableFlooding ="false"/ enableDischaring ="false"TypeOK == / b1Req in {"","INIT","ACCEPTED","PROCESSING","WAIT","FLOODING","DISCHARGING","SUCCESS","FAIL"} / b2Req in {"","INIT","ACCEPTED","PROCESSING","WAIT","FLOODING","DISCHARGING","SUCCESS","FAIL"} / ~(b1Req /="SUCCESS"/ b2Req ="SUCCESS") / ~(b1Req ="SUCCESS"/ b2Req ="WAIT") / enableFlooding in {"true","false"} / enableDischaring in {"true","false"} saveB1 == / b1Req =""/ b1Req ="INIT"/ UNCHANGED <> saveB2 == / b2Req =""/ b2Req ="INIT"/ UNCHANGED <> * receive B1 request receiveB1 == / b1Req ="INIT"/ IF enableFlooding ="true"THEN b1Req ="FLOODING"ELSE b1Req ="ACCEPTED"/ UNCHANGED <> * recieve B2 request receiveB2 == / b2Req ="INIT"/ IF enableFlooding ="true"THEN IF b1Req ="SUCCESS"THEN b2Req ="FLOODING"ELSE b2Req ="WAIT"ELSE IF b1Req ="SUCCESS"THEN b2Req ="ACCEPTED"ELSE b2Req ="WAIT"/ UNCHANGED <> * process B1 processB1 == / b1Req in {"ACCEPTED","DISCHARGING"} / b1Req ="PROCESSING"/ UNCHANGED <> * process B2 processB2 == / b2Req in {"ACCEPTED","DISCHARGING"} / b2Req ="PROCESSING"/ UNCHANGED <> notifyB1 == / b1Req ="PROCESSING"/ b1Req ="SUCCESS"/ IF b2Req ="WAIT"THEN IF enableFlooding ="true"THEN / b2Req ="FLOODING"/ UNCHANGED <> ELSE / b2Req ="ACCEPTED"/ UNCHANGED <> ELSE UNCHANGED <> notifyB2 == / b2Req ="PROCESSING"/ b2Req ="SUCCESS"/ UNCHANGED <> dischargeB1 == / b1Req ="FLOODING"/ enableDischaring ="true"/ b1Req ="DISCHARGING"/ UNCHANGED <> dischargeB2 == / b2Req ="FLOODING"/ enableDischaring ="true"/ b2Req ="DISCHARGING"/ UNCHANGED <> floodingOn == / enableFlooding ="false"/ enableFlooding ="true"/ UNCHANGED <> floodingOff == / enableFlooding ="true"/ enableFlooding ="false"/ UNCHANGED <> dischangeOn == / enableDischaring ="false"/ enableDischaring ="true"/ UNCHANGED <> dischangeOff == / enableDischaring ="true"/ enableDischaring ="false"/ UNCHANGED <> Next == / saveB1 / saveB2 / receiveB1 / receiveB2 / notifyB1 / notifyB2 / processB1 / processB2 / dischargeB1 / dischargeB2 / floodingOn / floodingOff / dischangeOn / dischangeOff ============================================================================= * Modification History * Last modified Mon Aug 03 17:20:10 CST 2020 by segeon * Created Mon Aug 03 14:54:40 CST 2020 by segeon其中enableFlooding, enableDischaring是表示是否开启蓄洪、泄洪的系统状态变量;b1Req, b2Req代表B1交易和B2交易的状态。
初始状态:b1Req = "", b2Req = "", enableFlooding = "false", enableDischaring = "false"
状态校验:TypeOK,检查所有可能的状态中,不存在(b1Req != "SUCCESS" && b2Req = "SUCCESS",B1请求不是成功,但B2请求成功了), 也不存在(b1Req = "SUCCESS" && b2Req = "WAIT",B1请求成功了,但B2挂起了)这两种结果
如果我们将notifyB1步骤改成如下实现:
notifyB1 == / b1Req ="PROCESSING"/ b1Req ="SUCCESS"/ IF b2Req ="WAIT"THEN IF enableFlooding ="true"THEN */ b2Req ="FLOODING"/ UNCHANGED <> ELSE / b2Req ="ACCEPTED"/ UNCHANGED <> ELSE UNCHANGED <>TLC Checker会报错,显示TypeOK状态校验失败,并且从状态变迁过程中,可以看出导致校验失败的原因。
总结
TLA+对于比较复杂分布式系统或者多线程程序的验证非常有用,一方面在编写TLA+规范的过程中,开发人员需要对系统行为进行抽象,本身对于更深刻理解问题有帮助;另一方面,通过实际运行TLA+规范,可以发现我们通过逻辑推演或者系统测试不容易发现的问题,在设计、系分阶段就系统正确性有一个验证;第三,通过抽象的形式化描述,便于第三方理解算法思路,而不用关注实现代码细节。