聚热点 juredian

医院检查中的TlA表示什么意思(tla是什么意思)

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

搜索建议:
热评

 【歌词】あなたの言叶 -inst...

腕を组んだ避暑地の散步で偶然出逢う教会のWedding朝の风に溶けこむ赞美歌しあわせそなふだり のぞいて行こうよちょうど誓いの言叶が响くしあわせ 分けてほしいあ...(展开)