TLA+ Specifying System (1)

概述

• 并發系統的正确性是很難證明的，因為異步點太多，人類的大腦不是為并發而進化的，并發系統的行為變化可能性太多
• 如果能夠把系統的狀态/行為抽象為時态邏輯（Temporal Logic），結借助CPU超強的算力，窮舉出所有可能的behavior（狀态序列）就可以判斷系統是否正确
• 基本的TLA+文法和使用可見狀态序列是指數級别，需要深入立即系統和TLA+對狀态進行剪枝
• 什麼是Temporal Logic：系統随着時間的推移，可能出現的狀态序列
• TLA+是基于數理邏輯的語言，如果你對數理邏輯很有研究，那麼會如魚得水

What is a specification?

• spec描述應該實作什麼，而不是描述如何實作
• 用來驗證設計，而不是教你如何設計
• 在動手coding之前，進行specify能幫助你更好的了解你的系統
• 隻驗證設計是否正确而不驗證性能
• specification的基礎是數學，因為隻有數學語言是精确的
• 這裡用到的數學是更加形式化的數學，而不是我們在學校時學到的經典數學（大部分也不是精确的）。形式化的數學看起來很冗長，但是能用最少的數學概念描述一個系統。

Why TLA+

• 1977年，艾米爾.伯努利用時序邏輯temporal logic來specify一個系統，但是隻能描述部分系統
• 1980年代，Lamport發明了TLA（temporal logical action），選擇了數學家們（而不是程式員）所喜愛的一階邏輯理論和集合理論
• TLA提供了specify系統的數學基礎，數學描述現實的系統，TLA來形式化數學：TLA就是來解決如何用程式描述數學的問題，而TLA+就是這門語言，僅僅借鑒了程式設計語言的子產品化的思想，除此之外都是數學概念
• TLA+可以友善描述任何離散的系統（因為它建立于集合論），尤其是異步系統
• TLA+使用簡潔的數學語言來描述狀态轉換
• TLA+不是用來描述程式執行的指令序列

一個例子

• C語言代碼

int i;
void main() {
    i = someNumber();
    i = I + 1;
}      

• 和這段代碼等價的spec是下面這段tla（emacs上可以安裝一個插件，以prity-print方式顯示希臘字元）


• 幾點說明：

• • TLA+支援以子產品方式組織代碼
  • 以——————————— MODULE SimpleProgram ----------------------開始
  • 以====================================================結尾
  • 任何TLA+ spce都要有Init和Next，Init和Next被稱為formula
  • TLA+會預設用Init進行初始化狀态，預設用Next疊代可能到達的狀态
  • Init == (pc = "start") /\ (i = 0), ‘==’ 定義一個 formula
  • 邏輯與運算符‘/\’：a /\ b 表示先發生a，再發生b
  • 邏輯或運算符‘/’：a / b 表示要麼發生a，要麼發生b
  • Next formula描述的是一個狀态機，‘/’運算連接配接起來的是兩個狀态入口“start”和“middle”
  • pc’ 和 i’ 是下一個狀态中pc和I的值，記做(pc primae, i prime)
  • TLA+ 使用寬度周遊，暴力周遊所有可達的狀态

總結

• 任何系統都能夠使用狀态機描述
• specify狀态機所有可達的狀态
• TLA+使用CPU超強的算力窮舉所有可能的狀态序列