最近在學併發開發, 裡面需要用到promela語言來檢測**的邏輯
promela用起來很麻煩, 不過網上有個windows gui程式, 裡面還帶了很多例子**, 稍微看看就可以懂了
安裝起來很簡單, 安裝好之後, 開啟安裝目錄下的config檔案, 吧mingw路徑配置好就可以了.
開啟程式執行, 隨便找個示例**跑下, 如果編譯不成功, 那麼就在他的run.bat前面加上這行
set path=%path%;c:/path_of_mingw/bin
你可以在安裝目錄下找到使用者手冊jspin-user.pdf
一般檢測併發**需要檢測下面三項
1.互斥(mutual exclusion)
2.無死鎖(free from deadlock)
3.無飢餓(free from starvation)
在這個工具裡面, 你可以用assert()來進行檢測, 也可以自己寫ltl(線性時間邏輯)來檢測,
你可以開啟裡面的 dekker.pml 學習下如何使用它們來檢測
pml語言的語法略奇葩,不過看看就會, active proctype 就是宣告乙個執行緒
/* dekker's algorithm */
bool wantp = false, wantq = false;
byte turn = 1;
bool csp = false, csq = false;
ltl
active proctype p()
active proctype q()
線性時間邏輯就是在邏輯的基礎上加上了時間的概念, 表示永遠是1, <>表示在未來終究會出現1 等等
dekker.pml中的
ltl
表示的意思就是
永遠會反反覆覆的進入p的critical section && 永遠會反反覆覆的進入q的critical section
這句話就是用來檢測starvation的, 如果程式有能力反覆執行p而不執行q(無論機率多麼小), jspin都會報錯
檢測ltl的時候請選擇acceptance模式.
測試starvation的時候去掉weak fairness
意思就是:允許乙個能夠反覆執行的程序無限反覆執行,每次都是他執行, 而不讓其他的程序執行(在現實的計算機cpu中是不現實的)
如果你的程式有了starvation freedom的話, 那麼就會保證上述的情況永遠不會出現
CSS入門教程
css是 cascading style sheets 的簡稱，中文翻譯為 串接樣式表 也有人翻譯為 樣式表 css用以作為網頁的排版和風格設計，在web標準建站中，對css的熟悉和使用是相當重要的乙個內容。css的作用是彌補html的不足，讓網頁的設計更為靈活。這個文章只是為您介紹css的基礎應用...
CSS入門教程
css是 cascading style sheets 的簡稱，中文翻譯為 串接樣式表 也有人翻譯為 樣式表 css用以作為網頁的排版和風格設計，在web標準建站中，對css的熟悉和使用是相當重要的乙個內容。css的作用是彌補html的不足，讓網頁的設計更為靈活。這個文章只是為您介紹css的基礎應用...
Linux入門教程
linux下有兩種使用者 1.root使用者，提示符 2.普通使用者，提示符 在 etc目錄下有乙個inittab檔案，其中有一行配置 id 3 defualt 其中，數字3就代表一啟動進入字元終端，如果改為5則代表一啟動進入x window 修改口令 passwd 退出登入 exit 關閉機器 只...