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+规范，可以发现我们通过逻辑推演或者系统测试不容易发现的问题，在设计、系分阶段就系统正确性有一个验证；第三，通过抽象的形式化描述，便于第三方理解算法思路，而不用关注实现代码细节。
