มาทำ formal proof การจัดการ atomic transactions ด้วยภาษา tla+ กันเถอะ

Nattawat Songsom

5 min readDec 29, 2022

มาจากหนึ่งใน series TLA+ tutorial ของ Lessie Lamport นะครับ

Atomic transactions คืออะไร ?

ลองมายกตัวอย่างจากงานแต่งงานกัน

เมื่อบาทหลวงถามว่าตกลงแต่งงานกันมั้ย

ไม่ว่าบ่าวสาวจะตอบว่าอะไร ผลลัพธ์การแต่งงานควรจะเป็นหนึ่งในสองเคสนี้คือ

1 ทั้งคู่ได้แต่งงานกัน

2 ทั้งคู่ไม่ได้แต่งงานกัน

โดยเคสที่ไม่ควรเกิดขึ้นคือ ฝ่ายหนึ่งแต่งงาน แต่อีกฝ่ายไม่ได้แต่งงานนั่นเอง

โอเค นั่นเป็นตัวอย่างของ atomic transaction ของการแต่งงาน

แต่ในการรัน sql command ก็สามารถทำ atomic transaction ได้เช่นกัน

เช่นจาก code Typeorm ด้านล่าง มีการ update db ด้วย 3 sql command แยกกัน

ซึ่งผลลัพธ์จะมีได้ 2 แบบเท่านั้นคือ

ทั้ง 3 sql command ทำสำเร็จ
ไม่มี sql command ใดเลยทำสำเร็จ

โดยในการพิสูจน์ ผลลัพธ์ สามารถทำได้ด้วยการหาว่า สามารถเกิดผลลัพธ์ที่ 1 ใน sql command ทำสำเร็จ และ อีก 1 ใน sql command ทำไม่สำเร็จ ได้หรือไม่

ถ้าสามารถเกิดขึ้นได้ แสดงว่า db transaction ไม่สามารถทำตาม concept atomicity ได้

State machine design

โอเค ถ้าเรามี process สำหรับรัน sql command ตัว process นี้ จะอยู่ในสถานะใดได้บ้าง

น่าจะได้ประมาณนี้

ยังไม่เริ่มรัน
รันอยู่
สำเร็จ
ไม่สำเร็จ

โดยเราจะแทนด้วยคำว่า

ยังไม่เริ่มรัน = working (กำลังทำอย่างอื่นอยู่)
รันอยู่ = prepared (รันอยู่ จะรอดู process อื่นว่าทำสำเร็จรึเปล่า)
สำเร็จ = commited (การรัน sql command สำเร็จ)
ไม่สำเร็จ = aborted (การรัน sql command ไม่สำเร็จ)

โดยเราสามารถวาดออกมาเป็น state diagram ได้ดังนี้

ซึ่งแน่นอนว่าเมื่อหลาย process run พร้อมกัน แต่ละ process ก็จะมี state ของตัวเอง

โดยในการทดสอบว่า transaction มีความ atomic มั้ยนั้น จะต้องจบที่ 1 ใน 2 case นี้คือ

ทุก process commited
ทุก process aborted

ซึ่งในการพิสูจน์ เราจะหาว่ามี case ที่ process นึง commited แต่อีก process aborted รึเปล่า ถ้ามี แสดงว่า transaction ไม่มีความ atomic

Let’s write TLA+

โอเค ในการขึ้น spec ใหม่ เราได้ดูไปแล้วใน part ที่แล้ว ดังนั้น part นี้เราจะมาเริ่มที่เขียน code กันเลย

มาเริ่มจากการ initial ค่าของแต่ละ resource manager

ในบรรทัด 2 เป็นการประกาศตัวแปร RM ไว้เก็บ state ปัจจุบัน ของ resource manager ทั้งหมด

ในบรรทัด 3 เป็นการประกาศตัวแปร rmState ไว้เข้าถึง state ของ resource manager แต่ละตัว

ในบรรทัด 6 เป็นการประกาศค่าเริ่มต้น โดยให้ทุกๆ resource manager มี state เป็น working

note: ใน tutorial เค้าใช้คำว่า resource manager แต่ผมใช้คำว่า process นะ สองอย่างนี้แทนตัวจัดการ sql command เหมือนกัน

note: syntax rmState = [ r \in RM |-> “working”] ทำงานยังไง ?

เราจะแบ่งเป็น 2 syntax ย่อย คือ

1 rmState = แปลว่า rmState เป็น array ที่มีสมาชิกคือ

2 [ r \in RM |-> “working”] แปลว่า array ที่มีค่าที่ index r ใดๆ เท่ากับ working

เมื่อเอามารวมกัน rmState = [ r \in RM |-> “working”] จะแปลได้ว่า rmState เป็น array โดยสมาชิกที่ index r ใดๆ เท่ากับ working

หรือก็คือ rmState = array ที่มีสมาชิกทุกตัวเป็น working นั่นเอง

โอเค เรา init ค่าเสร็จละ

ทีนี้การเปลี่ยน state ของแต่ละ node ต้องมีเงื่อนไขยังไง เพื่อให้ตรงตามสมมติฐานที่เราตั้งไว้ ?

มาลองเขียนแบบผิดๆกันก่อน จะได้เรียนการแก้ bug ไปด้วยเลย

โอเค มาเริ่มจากการประกาศเงื่อนไขในการเปลี่ยนแปลง state

โดยจากรูป

state working สามารถเปลี่ยนเป็น prepared ได้

state working และ prepared สามารถเปลี่ยนเป็น aborted ได้

state prepared สามารถเปลี่ยนเป็น commited ได้

โดยจากที่กล่าวมา สามารถเขียน code ได้ดังนี้

บรรทัดที่ 11–12 คือ ถ้า state ปัจจุบันของ resource manager เป็น working แล้ว state ต่อไปสามารถเป็น prepared ได้

บรรทัดที่ 14–17 คือ ถ้า state ปัจจุบันของ resource manager เป็น prepared แล้ว state ต่อไปสามารถเป็น committed ได้

หรือ

ถ้า state ปัจจุบันของ resource manager เป็น working หรือ prepared แล้ว state ต่อไปสามารถเป็น aborted ได้

บรรทัดที่ 19 คือ ในรัน 1 step ของทั้งระบบ จะมีการเปลี่ยน state ของ resource manager ตัวใดตัวหนึ่ง ตามเงื่อนไขใด เงื่อนไขหนึ่งต่อไปนี้ นั่นคือ

ถ้า state ปัจจุบันของ resource manager เป็น working แล้ว state ต่อไปสามารถเป็น prepared ได้
ถ้า state ปัจจุบันของ resource manager เป็น prepared แล้ว state ต่อไปสามารถเป็น committed ได้ หรือ ถ้า state ปัจจุบันของ resource manager เป็น working หรือ prepared แล้ว state ต่อไปสามารถเป็น aborted ได้

note: rmState’ = คือ state ต่อไปของ rmState มีค่าเป็น …

note: syntax [rmState EXCEPT ![r] = “prepared”] มีความหมายดังนี้

rmState ณ index ที่ r มีค่าเป็น prepared

โดยสามารถเขียนเป็น if else ได้ตามรูป

note: syntax TCNext == \E r \in RM : Prepare(r) \/ Decide(r) มีความหมายดังนี้

ในการรัน step ต่อไป resource manager ตัวใดตัวหนึ่งจะเปลี่ยน state ตาม ที่ระบุใน Prepare หรือ Decide

โดยสามารถเขียนเป็นรูปได้ตามนี้

จะสังเกตุว่าในการรัน step ต่อไป Prepare(“r1”) Decide(“r1”) Prepare(“r2”) … Decide(“r4”) อย่างใดอย่างหนึ่งนี้ ต้องมีการรันเกิดขึ้น

โอเค เขียน spec เสร็จละ มาเขียนบทพิสูจน์กัน

เริ่มจากการ check ว่า state ของ resource manager ไม่หลุด range มั้ย

จากนั้นเช็คว่าในทุกๆ resource manager มี resource manager คู่ใดรึเปล่าที่มีค่าเป็น committed และ aborted ในเวลาเดียวกัน

โอเค code เต็มๆก็ประมาณนี้

เอาละ มารันด้วย TLA+ toolbox กัน

การ setup toolbox เราเคยเขียนไปในบทความก่อนๆแล้ว จะข้ามไปเลยนะ

เริ่มจากการ setup Init และ Next syntax รวมถึงการกำหนดจำนวน resource manager ในการทดสอบ โดยเราจะใช้ 3 ตามรูป

จากนั้นกำหนดเงื่อนไขในการทดสอบ เราจะใช้ 2 เงื่อนไขที่เพิ่งเขียนไปตามรูป

โอเค รันแล้วเป็นยังไงบ้าง ?

เราจะพบว่า resource manager คู่หนึ่งสามารถเป็น committed และ aborted พร้อมกันได้ ตามรูป

เอาละ แสดงว่าเรา design ระบบผิด แล้วเราจะป้องกันไม่ให้เกิด case นี้ได้ยังไงบ้าง ?

โอเค มาลองยกตัวอย่างกัน เช่น จากรูป

ถ้า resource manager 1 เป็น aborted แล้ว การเปลี่ยนสถานะของ resource manager 2 จาก prepared เป็น committed ควรจะทำได้รึเปล่า ?

คำตอบคือไม่

ดังนั้นสามารถเขียนเพิ่มได้ดังนี้

โดยในบรรทัดที่ 1 คือ เงื่อนไขในการเช็คว่า ทุกๆ resource manager มีสถานะเป็น prepared หรือ commited รึเปล่า

ในบรรทัดที่ 10 คือ เราเพิ่มเงื่อนไขมาว่า การเปลี่ยนสถานะจาก prepared เป็น commited จะต้องเช็คก่อนว่า ทุกๆ resource manager มีสถานะเป็น prepared หรือ commited รึเปล่า

โอเค มายกตัวอย่างอีกเงื่อนไขกัน

ถ้า resource manager เป็น committed แล้ว เราควรปล่อยให้ resource manager 2 เปลี่ยนสถานะจาก prepared เป็น aborted รึเปล่า