Luận văn -Phương pháp kiểm chứng tính đúng đắn của một chương trình Java đa luồng thông qua sử dụng logic Hoare

ớp của các đối tác đang giao tiếp, và các điều kiện trước của các lệnh đang giao tiếp là đúng trước giao tiếp. Đối với sự thi hành phương thức, điều kiện trước của phương thức được gọi là bất biến lớp của nó. Hai lệnh đại diện các đối tác đang giao tiếp được nắm giữ bởi khẳng định comm, phụ thuộc vào kiểu của giao tiếp: Với sự thi hành phương thức  me0 , khẳng định   '0 zzE  phát biểu rằng giá trị của z’ nhận dạng đối tượng được gọi. Chú ý rằng sự thi hành phương thức điều khiển thông qua sự trả về địa chỉ như là một tham biến phụ trợ, và các giá trị của các tham biến hình thức còn lại không được thay đổi. Hơn nữa, các tham biến không thể chứa các biến thể hiện, nghĩa là, thể hiện của chúng không thay đổi trong suốt quá trình thi hành phương thức. Bởi vậy, các tham biến hình thức và các tham biến thực sự có thể được sử dụng trong sự trả về từ một phương thức để nhận dạng các đối tác đang trong mối quan hệ caller- - 38 - callee, bằng cách sử dụng các biến phụ trợ. Do đó với trường hợp trả về, comm thêm vào phát biểu  zEu  , trong đó u và e là các biến hình thức và biến thực sự. Sự trả về từ phương thức run kết thúc luồng đang thi hành; phương thức run không có các kết quả với giao tiếp. Các thay đổi trạng thái được biểu thị bởi các phép gán. Ví dụ của sự thi hành một phương thức, giao tiếp được phát biểu bởi các phép gán  zEu : , trong đó sự khởi tạo của các biến cục bộ v được bao hàm bởi  vInitv :' . Các phép gán  zEyz 11 :.  và  '':''. 22 zEyz  đại diện cho các quan sát gọi và quan sát được gọi 11 : ey và 22 : ey , theo thứ tự được thi hành trong z và z’. Định nghĩa 2.4.14. (Kiểm tra sự hợp tác: Sự giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác với giao tiếp, nếu G|         nullznullzcommzIzQzIzPGI cc  '''' '11 commf     ''22 zQzP  và (2.6) G|         nullznullzcommzIzQzIzPGI cc  '''' '11 21;; obsobscomm fff (2.7)     ''33 zQzPGI  là đúng với các biến logic mới khác nhau cLVarz và '' cLVarz  , trong các trường hợp sau: 1.CALL: Với tất cả các lệnh       waitcallcallret peypemeup 3 ! 11 ! 201 :.:  (hoặc là các lệnh này mà không nhận một giá trị) trong lớp c với 0e của kiểu c’, trong đó phương thức m của c’ có thân     ret callcall ereturnstmqeyq ;: 3 ? 22 ? 2  , các tham biến hình thức u , và các biến cục bộ v trừ các tham biến hình thức. Bất biến của lớp được gọi là '1 cIq  . Khẳng định comm được cho bởi   '0 zzE  . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf là  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . - 39 - 2. RETURN: Với tất cả        3 ? 44 ? 21 ! 0 :.: peyppstmemeu retretwaitcall ret  hoặc không nhận một giá trị đang xuất hiện trong c với 0e của kiểu c’, sao cho phương thức m của c’ có lệnh trả về      3 ! 33 ! 21 : qeyqereturnq retret ret  , và danh sách biến hình thức u , các phương trình trên phải là đúng với comm được cho bởi    zEuzzE  ''0 , và trong đó commf là  '': zEu retret  , 1obsf là  '':''. 33 zEyz  , và 2obsf là  zEyz 44 :.  . 3. runRETURN : Với      3 ! 33 ! 21 : qeyqreturnq retret  đang xuất hiện trong phương thức run của lớp chính, trueppp  321 , truecomm  , và hơn nữa commf và 2obsf là các lệnh rỗng, và 1obsf là  '':''. 33 zEyz  . Bên cạnh các lời gọi phương thức và các trả về phương thức, kiểm tra sự hợp tác cần điều khiển Ví dụ 2.4.15. Ví dụ này minh họa cách chứng minh các thuộc tính của việc truyền tham biến. Cho    evmep ,.0 , với p được cho bằng v > 0, là một lệnh được chú thích trong lớp c với 0e của kiểu c’, và cho phương thức  ,um của c’ có thân của dạng   returnstmq ; trong đó q là u > 0. Tính quy nạp của phác thảo chứng minh yêu cầu rằng nếu p là đúng trước khi gọi (bên cạnh sự đúng đắn của các bất biến toàn cục và bất biến lớp), thì q được thỏa mãn sau sự thi hành. Điều kiện 2.7 của kiểm tra sự hợp tác yêu cầu chứng minh      '':'| zQvuzPG  , khai triển thành    0':'0|  uvuvG . Ví dụ 2.4.16. Ví dụ sau chứng minh cách biểu thị sự phụ thuộc giữa các trạng thái thể hiện trong cấu hình toàn cục và sử dụng thông tin này trong kiểm tra giao tiếp. Cho    emep .0 , với p được cho bằng oex  00 , là một lệnh được chú thích trong lớp c với 0e của kiểu c’, x là một biến thể hiện kiểu nguyên, và o là một biến thể hiện của kiểu c’, và cho phương thức  um của c’ có chú thích thân phương thức   returnstmq ; trong đó q là y > 0 và y là một biến thể hiện kiểu nguyên. Hơn nữa cho cLVarz và cho bất biến toàn cục được cho bằng   0..0...  yozxznulloznullzz . Tính quy nạp yêu cầu rằng nếu p và bất biến toàn cục là đúng trước khi gọi, thì q được thỏa mãn sau sự thi hành. Điều kiện 2.7 của kiểm tra sự hợp tác     0..0...| yozxznulloznullzzG - 40 -      nullznullzzzEozzExz  ''.0. 00  zEu :'  0'. yz tạo đối tượng lượng hóa bằng z, mệnh đề kéo theo ozzyoz .'0..  , có nghĩa là 0'. yz . Bên cạnh các lời gọi phương thức và các sự trả về, kiểm tra sự hợp tác yêu cầu quản lý tạo đối tượng, duy trì các bất biến toàn cục, điều kiện sau của lệnh new và quan sát của nó, và các bất biến lớp của của đối tượng mới. Ta có thể giả thiết rằng điều kiện trước của lệnh tạo đối tượng, bất biến lớp của đối tượng tạo, và bất biến toàn cục là đúng trong cấu hình trước khi tạo đối tượng. Sự mở rộng của trạng thái toàn cục với đối tượng được tạo mới được đưa ra trong điều kiện sau mạnh nhất, có nghĩa là, nó được yêu cầu là đúng ngay sau khi tạo đối tượng. Ta sử dụng lượng hóa tồn tại để tham chiếu tới giá trị cũ: z’ của kiểu listObjectLVar đại diện các đối tượng đang tồn tại trước khi mở rộng. Hơn nữa, định danh đối tượng được tạo ra được lưu trữ trong u là mới và thể hiện mới có thể được khởi tạo được biểu thị bằng khẳng định toàn cục  uzFresh ,' được định nghĩa là     uvzvObjectvzuuInitState  '.:' . Để biểu thị rằng một khẳng định tham chiếu tới tập các đối tượng đang tồn tại trước sự mở rộng của trạng thái toàn cục, ta chỉ cần giới hạn lượng hóa phổ biến trong khẳng định tới dãy thông qua các đối tượng từ z’. Cho P là một khẳng định toàn cục và listObjectLVarz ' là một biến logic không xuất hiện trong P. Thì 'zP  là khẳng định toàn cục với tất cả các lượng hóa '. Pz được thay thế bằng   ''. Pzzobjz  , trong đó obj(v) ký hiệu tập các đối tượng xuất hiện trong giá trị v. Bổ đề 2.4.18. Giả thiết rằng một trạng thái toàn cục  , một sử mở rộng  initcinst ,'   đối với   ValVal c  , , và một môi trường logic  chỉ tham chiếu tới các giá trị đang tồn tại trong  . Cho v là dãy bao gồm tất cả các phần tử của  nullcc Val . Thì đối với tất cả các khẳng định P và các biến logic listObjectLVarz ' không xuất hiện trong P, PG|, khi và chỉ khi   '|',' zPvz G   . Vị từ   '. zPu  được ước lượng ngay sau khi tạo đối tượng cnewu : , biểu thị rằng P đúng trước khi tạo đối tượng mới. - 41 - Định nghĩa 2.4.19. (Kiểm tra sự hợp tác: Tạo đối tượng) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với việc tạo đối tượng, nếu với tất cả các lớp c’ và các lệnh      321 :: peypnewup newnewc  trong c’: G|         '.,''. '1 zzIzPuGIuzFreshzuznullz c     uIzP c 2 và G|          '.,''. '1 zzIzPuGIuzFreshzuznullz c   zEyz :.   zPGI 3 là đúng với 'cLVarz và listObjectLVarz ' mới. - 42 - CHƯƠNG 3. NGÔN NGỮ TƯƠNG TRANH 3.1. Cú pháp  startmethmethmethcclassclass runmeth...:: classclass main :: mainclassclassclassprog ...:: Ta tập trung vào khía cạnh tương tranh, tất cả các lớp là các lớp Thread theo nghĩa của Java: Mỗi lớp chứa một phương thức start được định nghĩa trước có thể được thi hành chỉ một lần đối với mỗi đối tượng, kết quả là tạo ra một luồng mới của sự thi hành. Luồng mới bắt đầu thi hành phương thức run được định nghĩa bởi người dùng của đối tượng được cho trong khi luồng ban đầu tiếp tục sự thi hành của nó. Phương thức run không thể được thi hành trực tiếp. Phương thức start không có tham biến không có giá trị trả về thì không được cài đặt một cách đúng cú pháp. Cú pháp không cho phép các tham chiếu hạn chế tới các biến thể hiện. Như là một hệ quả, các biến chia sẻ tương tranh được tạo ra bởi sự thi hành tương tranh chỉ trên một đối tượng duy nhất, không phải thông qua tập các đối tượng. 3.2. Ngữ nghĩa Các ngữ nghĩa toán tử của concJava mở rộng các ngữ nghĩa của seqJava bởi tạo các luồng động. Các quy tắc thêm:                 start c CALL stmstarteT stmstarteTstartedVale      ,;.,, ,;.,,,        ,,,,,, ,, cruncruninit bodystmT                     skip startCALLstmTstmstarteT stmstarteTstartedVale    ,,,,;.,, ,;.,,,     Sự thi hành phương thức start tạo ra một luồng mới bắt đầu thi hành phương thức run của đối tượng được gọi. Chỉ có lần gọi đầu tiên thi hành phương thức start có hiệu quả (quy tắc skipstartCALL ). Vị từ  ,Tstarted là đúng khi và chỉ khi tồn tại một ngăn - 43 - xếp có dạng  000 ,, stm  111 ,, stm …  nnn stm,,  T sao cho 0  . Một luồng kết thúc vòng đời của nó bằng sự trả về từ một phương thức run. 3.3. Hệ chứng minh 3.3.1. Phác thảo chứng minh Để đạt được một hệ chứng minh đầy đủ, đối với ngôn ngữ tương tranh ta phải có khả năng nhận dạng các luồng. Ta nhận dạng một luồng qua đối tượng mà trong đó nó bắt đầu sự thi hành. Do đó ta sử dụng kiểu Thread như là sự viết tắt cho kiểu Object. Một định danh là duy nhất, bởi vì một luồng của đối tượng chỉ có thể được bắt đầu một lần. Trong suốt một lời gọi phương thức, luồng phương thức được gọi nhận định danh của nó như là tham biến phụ trợ hình thức được tích hợp thread. Ta mở rộng tham biến hình thức phụ trợ caller bằng định danh luồng gọi, nghĩa là, cho caller là kiểu ThreadIntObject  , lưu trữ các định danh của đối tượng của luồng gọi, lời gọi cấu hình cục bộ, và luồng gọi. Chú ý các định danh luồng của đối tượng gọi và đối tượng được gọi là như nhau trong tất cả các trường hợp ngoại trừ đối với sự thi hành của phương thức start. Phương thức run của đối tượng ban đầu được thi hành với các tham biến  callerthread , có các giá trị   nullnull ,0,,0 , trong đó 0 biểu thị đối tượng ban đầu. Giá trị của biến thể hiện phụ trợ được tích hợp vào started nhớ bất kỳ khi nào phương thức start của đối tượng đã được thi hành. Theo cú pháp, mỗi danh sách tham biến hình thức u trong chương trình gốc được mở rộng thành  callerthreadu ,, . Tương ứng với phương thức gọi, mỗi danh sách tham biến thực sự e trong các câu lệnh thi hành một phương thức khác với phương thức start được mở rộng thành   threadconfthisthreade ,,,, . Sự thi hành của phương thức start không có tham biến của đối tượng 0e lấy danh sách tham biến thực sự   threadconfthise ,,,0 . Sự quan sát của phương thức được gọi ở điểm bắt đầu của phương thức run thi hành started := true. Các biến conf và counter cũng được cập nhật. Bởi vì một luồng gọi phương thức start không đợi sự trả về của phương thức start nhưng tiếp tục thi hành, sự bổ sung và chú thích của sự thi hành phương thức start có dạng là        3!!201 . pstmpestartep callcall . 3.3.2. Kiểm chứng các điều kiện Tính đúng đắn ban đầu - 44 - Tính đúng đắn cục bộ chỉ thay đổi ở chỗ các tham biến hình thức thread và caller được gán các giá trị ban đầu  và  nullnull ,0, , trong đó  là đối tượng ban đầu. Định nghĩa 3.3.1. (Tính đúng đắn ban đầu) Cho thân của phương thức run của lớp chính c là     returnstmpeyp callcall ;: 3 ? 22 ? 2  với biến cục bộ v không có các tham biến hình thức, cLVarz , và ObjectLVarz ' . Một phác thảo chứng minh là đúng đắn ban đầu, nếu G|   ''.' zznullzzzInitState     nullnullzvInitcallerthreadv ,0,,,:,,    zP2 , và G|   ''.' zznullzzzInitState       zEyznullnullzvInitcallerthreadv 22 :.;,0,,,:,,      zIzPGI c 3 . Khẳng định   '''. zznullzzzInitState  phát biểu rằng trạng thái toàn cục ban đầu định nghĩa một đối tượng z đang tồn tại trong trạng thái thể hiện ban đầu của nó, và quan sát 22 : ey  ở phần bắt đầu của phương thức run của đối tượng ban đầu z được thể hiện bởi phép gán  zEyz 22 :.  . Sự khác nhau là ở trong sự khởi tạo của cấu hình cục bộ, cấu hình cục bộ bây giờ được biểu diễn bởi phép gán    0,0,,,:,, nullthreadvInitcallerthreadv  . Kiểm tra tính không có can thiệp Sự can thiệp của một luồng duy nhất dưới sự thi hành của nó giống như trong ngôn ngữ tuần tự. Tuy nhiên, ta phải giải quyết với sự bất biến của các thuộc tính của một luồng dưới sự thi hành của một luồng khác. Một khẳng định q tại một điểm điều khiển phải là bất biến dưới một phép gán ey : trong cùng một lớp nếu cấu hình cục bộ được mô tả bởi khẳng định không hoạt động trong bước tính toán đang thi hành phép gán. Để phân biệt các biến cục bộ của các cấu hình cục bộ khác nhau, ta đặt lại tên của các biến cục bộ trong khẳng định mà phải là bất biến, có kết quả là các biến, các biểu thức, và các khẳng định được đánh - 45 - dấu phẩy. Ví dụ, trong các điều kiện ta sử dụng thread để nhận dạng luồng đang thi hành phép gán, và thread’ để nhận dạng luồng được mô tả bởi q. Nếu q và ey : thuộc về cùng một luồng, có nghĩa là , thead’ = thread, thì ta có cùng mệnh đề như đối với ngôn ngữ tuần tự. Nếu khẳng định và phép gán thuộc về các luồng khác nhau, tính không có can thiệp phải được biểu diễn trong tất cả các trường hợp trừ sự thi hành chính nó của phương thức start: Quan sát được gọi của một sự thi hành chính nó của phương thức start không thể can thiệp với điều kiện trước của sự thi hành. Để mô tả sự thiết lập này, ta định nghĩa  eyqstartself :,_ bằng  ',', threadconfthiscaller  khi và chỉ khi q là điều kiện trước của sự thi hành phương thức  estarte .0 và phép gán là quan sát được gọi tại phần bắt đầu của phương thức run, và bằng false nếu ngược lại. Định nghĩa 3.3.2. (Tính không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu các điều kiện của định nghĩa 2.4.1 đúng với  eyqretforwaits :,__ được thay thế bằng   defe :yq,interferes thread = thread’   eyqretforwaits :,__  eyqstartselfthreadthread  :,_' Ví dụ 3.3.3. Giả thiết một lệnh gán được chú thích  stmp trong một phương thức, và một khẳng định q tại một điểm điều khiển không đợi sự trả về trong cùng một phương thức, sao cho p và q kéo theo thread = this. Điều này có nghĩa là, phương thức được thì hành chỉ bởi luồng của đối tượng mà phương thức đó thuộc về. Rõ ràng, p và q không thể đồng thời đạt tới được bằng cùng một luồng. Đối với tính bất biến của q dưới phép gán stm, mệnh đề của điều kiện không có can thiệp kéo theo  stmqqp ,interferes' . Từ 'qp  ta kết luận thread = thread’, và do đó bằng định nghĩa của  e:yq,interferes khẳng định q là một điểm điều khiển chờ trả về, nhưng trong trường hợp này thì không đúng, và do đó mệnh đề của điều kiện ước lượng là sai. Kiểm tra sự hợp tác Kiểm tra sự hợp tác đối với tạo đối tượng không bị ảnh hưởng bởi việc thêm vào tính tương tranh. Sự thi hành của các phương thức khác với phương thức start, được thi hành bởi một luồng duy nhất, không bị ảnh hưởng bởi sự có mặt của tính tương tranh. z và z’ là các biến logic mới đại diện cho đối tượng gọi và đối tượng được gọi. Bên - 46 - cạnh điều kiện trước của lời gọi, các bất biến toàn cục, bất biến lớp, ta giả sử rằng sự thi hành được cho phép, có nghĩa là, luồng của đối tượng được gọi chưa được bắt đầu, được định nghĩa bằng startedz'. . Định nghĩa 3.3.5. (Kiểm tra sự hợp tác: Giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với sự giao tiếp, nếu các điều kiện của định nghĩa 2.4.14 đúng đối với các lệnh được liệt kê ở đó với startm  , và thêm vào các trường hợp sau: 1. startCALL : Đối với tất cả các lệnh       3 ! 11 ! 201 :. peypestartep callcall  trong lớp c với 0e của kiểu c’, comm được cho bằng   startedzzzE '.'0  , trong đó     returnstmqeyq callcall ;: 3 ? 22 ? 2  là thân của của phương thức run của c’ có các tham biến hình thức u , và các biến cục bộ v trừ các tham biến hình thức. Bất biến của lớp được gọi là '1 cIq  . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf là  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . 2. skipstartCALL : Đối với các lệnh phía trên, các phương trình phải đúng với khẳng định comm được cho bằng   trueqqstartedzzzE  320 ,'.' , 1q và 1obsf như phần trên, và commf và 2obsf là lệnh rỗng. - 47 - CHƯƠNG 4. BỘ ĐIỀU PHỐI LẶP LẠI 4.1. Cú pháp Các phương thức được bao bọc bởi một từ bổ nghĩa modif phân biệt giữa các phương thức đồng bộ và không đồng bộ. Trong phần tiếp theo ta tham chiếu tới các lệnh trong thân của một phương thức đã đồng bộ như là đang được đồng bộ. Do vậy, ta xem các phương thức thêm vào được định nghĩa trước là wait, notify, và notifyAll modif ::= nsyn | sync meth ::= modif m (u, …, u) { stm; return retexp } runmeth ::= nsync run () { stm; return} waitmeth ::= nsync wait () { ?signal; getlockreturn } notifymeth ::= nsync notify () {!signal; return } notifyAllmeth ::= nsync notifyAll () { !signal_all; return } predefmeth ::= notifyAllnotifywaitstart methmethmethmeth class ::= class c { meth … meth predefrun methmeth } mainclass ::= class prog ::= class … class mainclass Các định nghĩa của cú pháp sử dụng các câu lệnh bổ trợ !sinal, !signal_all, ?signal, và getlockreturn mô tả ở mức cao của kỹ thuật trừu tượng hóa signal-and- continue dưới các phương thức wait, notify, và notifyAll. 4.2. Ngữ nghĩa Các ngữ nghĩa toán tử mở rộng các ngữ nghĩa của concJava bằng các quy tắc sau, trong đó quy tắc CALL được thay thế. Đối với các lời gọi phương thức được đồng bộ hóa, khóa của đối tượng được gọi phải là tự do hoặc được sở hữu bởi luồng đang thi hành, do vậy được biểu thị bởi vị từ owns, được định nghĩa bên dưới. - 48 - Các quy tắc còn lại quản lý các ngữ nghĩa của các phương thức điều phối wait, notify, và notifyAll. Trong cả ba trường hợp luồng gọi phải sở hữu khóa của đối tượng được gọi (quy tắc monitorCALL ). Một luồng có thể khóa chính nó trong một đối tượng mà nó sở hữu khóa bằng cách thi hành phương thức wait của đối tượng, do đó nó giải phóng khóa và đưa chính nó vào trong tập đợi của đối tượng. Tập đợi  ,Twait của một đối tượng được cho như là một tập của tất cả các ngăn xếp trong T với một phần tử ở đỉnh ngăn xếp có dạng  stmsignal;?,, . Sau khi đóng băng chính nó, luồng đợi thông báo từ luồng thi hành phương thức notify của đối tượng. Câu lệnh !signal trong phương thức notify do đó kích hoạt lại một luồng duy nhất được chọn đang chờ thông báo trong đối tượng được cho (quy tắc SIGNAL). Tương tự như tập chờ, tập được thông báo  ,Tnotified của đối tượng  biểu thị tập tất cả các ngăn xếp trong T với phần tử ở đỉnh ngăn xếp có dạng  getlockreturn,, , nghĩa là, các luồng được thông báo và cố gắng giữ khóa lại. Theo quy tắc waitRETURN , luồng được thông báo chỉ có thể tiếp tục thi hành getlockreturn sau thông báo nếu khóa là tự do. Chú ý rằng luồng thông báo không được bàn giao lại khóa cho một luồng đang được thông báo nhưng tiếp tục sở hữu nó. Hành vi này được biết đến như là quy tắc điều phối signal-and-continue. Các quy tắc:      cMethbodyumnotifyAllnotifywaitrunstartm  modif,,,,               ,,,0 ' euVale cminitc          CALLstmemeuT Towns     ,;.:,, ,syncmodif 0      ,,',;,, bodystmureceiveT   notifyAllnotifywaitm ,,                monitor c CALL stmmeT stmmeownsVale      ,;.,, ,;.,,,        ,,,;,, ,, cmcminit bodystmreceiveT  - 49 -        waitgetlock RETURN returnstmreceiveT Towns     ,,',;,, ,     ,,, stmT        SIGNAL stmsignalstmsignalT  ,';?,',';!,,        ,',',',, stmstmT          skip SIGNAL stmTstmsignalT Twait   ,,,,;!,, ,            SIGNALALL stmTstmallsignalT TsignalT   ,,,',;_!,, ,'    Nếu không có luồng nào đang đợi trong đối tượng, lệnh !signal của luồng thông báo không có kết quả (quy tắc skipSIGNAL ). Phương thức notifyAll tổng quát phương thức notify ở chỗ thông báo tất cả các luồng đang đợi được thông báo qua sự quảng bá !signal_all (quy tắc SIGNALALL). Kết quả của câu lệnh này được cho bởi định nghĩa  ,Tsignal là           ,;?,,|,,,\ TwaitstmsignalstmTwaitT  . Bằng cách sử dụng các tập đợi và tập được thông báo, ta có thể hình thức hóa vị từ owns: Một luồng  sở hữu khóa của đối tượng  khi và chỉ khi  thi hành phương thức đồng bộ của đối tượng  , nhưng không phải phương thức wait của nó. Vị từ owns (T,  ) là đúng khi và chỉ khi tồn tại một luồng T và một cấu hình    stm,, với stm được đồng bộ hóa và     ,, TnotifiedTwait  . 4.3. Hệ chứng minh 4.3.1. Phác thảo chứng minh Để nắm bắt sự loại trừ lẫn nhau và quy tắc điều phối, biến thể hiện được tích hợp thêm lock có kiểu IntThread  lưu trữ định danh của luồng sở hữu khóa, nếu có, cùng với số của các lời gọi đồng bộ trong chuỗi lời gọi của luồng sở hữu khóa. Giá trị ban đầu - 50 - của khóa 0) (null, free  biểu thị rằng khóa tự do. Các biến thể hiện wait và notified của kiểu  IntThread list là tương đương với các tập wait và notified của các ngữ nghĩa và lưu trữ các luồng đang đợi ở một bộ điều phối, theo thứ tự các luồng được thông báo. Bên cạnh định danh luồng, số của các lời gọi đồng bộ cũng được lưu trữ. Nói cách khác, các biến này nhớ giá trị của khóa cũ trước khi tạm thời ngừng, giá trị này được trả lại khi luồng hoạt động trở lại. Tất cả các biến bổ trợ được khởi tạo một cách bình thường. Đối với các giá trị thread của kiểu Thread và wait của kiểu list ( IntThread  ), ta sẽ viết waitthread  thay vì   waitnthread , với các giá trị n. Theo cú pháp, bên cạnh bổ sung được tích hợp của chương trước, quan sát được gọi ở điểm đầu và điểm cuối của mỗi thân phương thức được đồng bộ hóa thi hành theo thứ tự  lockinclock : và  lockdeclock : . Các ngữ nghĩa của sự tăng khóa      ,instlockinc là   1, nthread đối với    nvlockinst , . Chú ý rằng định danh của luồng sở hữu khóa không những trong trường hợp khóa tự do mà còn trong trường hợp nếu có một luồng đang sở hữu khóa. Tuy nhiên, bởi vì những cập nhật này được thi hành trong các phương thức được đồng bộ, nên các ngữ nghĩa đảm bảo cho trường hợp có một luồng đang sở hữu khóa, luồng sở hữu khóa là luồng đang thực thi, nghĩa là, nếu khóa không tự do thì thành phần luồng của khóa không được sửa đổi. Điều này có nghĩa là, tăng giá trị khóa  n, tạo ra  1, n , trong khi đó tăng một khóa tự do  0,null bởi một luồng  có kết quả là  1, . Giảm khóa  lockdec được thực hiện ngược lại:      ,instlockdec với    nlockinst ,  là  1, n nếu n > 1, và tự do nếu ngược lại. Thay vì các câu lệnh phụ trợ của các ngữ nghĩa, thông báo được thể hiện trong hệ chứng minh dựa trên trạng thái bởi các phép gán phụ trợ trong các biến wait và notified: Các câu lệnh phụ trợ !signal và !signal_all được thay thế bởi các phép gán phụ trợ. Các câu lệnh phụ trợ ?signal không được thể hiện. Điều này có nghĩa là, thông báo được thể hiện bởi duy nhất một phép gán phụ trợ được thi hành bởi luồng đưa ra thông báo. Đối với các luồng đang được thông báo, các điểm điều khiển trước và sau thông báo được mô tả bởi duy nhất một khẳng định trong phương thức wait. Các điểm điều khiển khác có thể được phân biệt bởi các giá trị của các biến phụ trợ tích hợp wait và notified. Vào phương thức wait nhận được quan sát   freelockwaitlockwait ,:,  trả về từ phương thức wait quan sát - 51 -     threadnotifiedgetnotifiedthreadnotifiedgetnotifiedlock ,\,,:,  . Đối với một luồng ThreadVal và một danh sách  IntthreadlistValnotified  ,  ,notifiedget lấy giá trị  n, từ danh sách. Các ngữ nghĩa đảm bảo tính duy nhất của sự kết hợp. Câu lệnh signal! của phương thức notify được thay thế bằng lệnh gán bội phụ trợ  notifiedwaitnotifynotifiedwait ,:,  , trong đó giá trị  notifiedwaitnotify , là một cặp của các tập được cho với một phần tử được chọn, được chuyển từ tập tập wait sang tập notified; nếu tập wait là rỗng, nó là định danh hàm. Cuối cùng, câu lệnh allsignal _! của phương thức notifyAll được thay thế bởi phép gán phụ trợ  ,:, waitnotifiedwaitnotified  . 4.3.2. Kiểm chứng các điều kiện Tính đúng đắn cục bộ và tính đúng đắn ban đầu thì như là đối với concJava . Đối với tính đúng đắn cục bộ, chú ý rằng các điều kiện bao hàm thêm vào tính bất biến đối với các luồng đang thi hành thông báo. Tuy nhiên, ta không cần thêm vào các điều kiện cho trường hợp này, bởi vì kết quả của thông báo được giữ lại bởi một phép gán phụ trợ. Đối với các luồng đang được thông báo, các điểm điều khiển trước và sau thông báo được mô tả bởi một khẳng định. Kiểm tra tính không có can thiệp Các phương thức được đồng bộ của một đối tượng duy nhất chỉ có thể được thi hành tương tranh nếu một trong các cấu hình cục bộ tương ứng đang chờ sự trả về: Nếu các luồng đang thi hành là khác nhau, thì một trong các luồng thi hành trong phương thức không được đồng bộ hóa wait của đối tượng; mặt khác, cả hai cấu hình cục bộ đang thi hành là trong cùng một dãy lời gọi. Định nghĩa 4.3.1. (Tính không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu các điều kiện của định nghĩa 3.3.2 đúng đối với tất cả các lớp c, tất cả các phép gán bội ey : với điều kiện p trong c, và tất cả các khẳng định q tại các điểm điều khiển trong c, sao cho hoặc là cả hai p và q không xuất hiện trong một phương thức đồng bộ, hoặc là q là một điểm điều khiển đang chờ sự trả về. Chú ý rằng đối với thông báo, ta cũng yêu cầu tính bất biến của các khẳng định của các luồng đang đợi thông báo. Thông báo được mô tả bằng một phép gán phụ trợ được thi hành bởi luồng thông báo. Điều đó có nghĩa là, cả hai tình trạng đang đợi và tình trạng được thông báo của một luồng bị tạm thời ngừng được thay thế bằng một điểm điều khiển duy nhất trong phương thức wait. Hai tình trạng có thể được phân biệt - 52 - bằng các giá trị của các biến wait và biến notified. Tính bất biến của điều kiện trước của lệnh trả về trong phương thức wait dưới phép gán trong phương thức notify biểu thị quá trình thông báo, trong khi đó tính bất biến của khẳng định thông qua các phép gán thay đổi khóa biểu thị kỹ thuật đồng bộ hóa. Thông tin về giá trị khóa được khai báo từ kiểm tra sự hợp tác bởi vì thông tin này phụ thuộc vào hành vi toàn cục. Ví dụ 4.3.2. Ví dụ này biểu diễn cách nhiều nhất một luồng có thể sở hữu khóa của một đối tượng có thể được sử dụng để biểu diễn sự loại trừ lẫn nhau. Ta sử dụng khẳng định  lockthreadowns , đối với   threadlockthreadnullthread  , trong đó  lockthread là thành phần đầu tiên của giá trị khóa. Cho  lockthreadforfree ,_ là   freelocklockthreadownsnullthread  , . Cho q, được cho bởi  lockthreadowns , , là một khẳng định tại một điểm điều khiển và cho   callcall stmp ?? với  lockthreadforfreep def ,_ là quan sát được gọi tại phần bắt đầu của một phương thức được đồng bộ hóa trong cùng lớp. Chú ý rằng quan sát stm thay đổi giá trị khóa. Điều kiện không có can thiệp     ',interferes'| qstmstmqqpL  đảm bảo tính bất biến của q dưới quan sát stm. Các khẳng định p và q’ kéo theo thread = thread’. Các điểm tại p và q chỉ có thể đạt tới được đồng thời bởi cùng một luồng nếu q mô tả một điểm đang chờ trả về. Nhưng điều đó là sai bởi định nghĩa của vị từ interferes: Nếu q không ở một điểm điều khiển đang chờ trả về, thì mệnh đề của điều kiện ước lượng là sai. Mặt khác, sau sự thi hành của lệnh phụ trợ tích hợp  lockinclock : trong stm ta có  lockthreadowns , , có nghĩa là  lockthreadowns ,' . Kiểm tra sự hợp tác Ta mở rộng kiểm tra sự hợp tác cho concJava với kỹ thuật đồng bộ hóa và với sự thi hành của các phương thức điều phối. Trong các ngôn ngữ trước, khẳng định comm phát biểu rằng các lệnh được cho đại diện các đối tác giao tiếp. Trong ngôn ngữ hiện tại với sự đồng bộ hóa điều phối, giao tiếp luôn luôn được cho phép. Do vậy khẳng định comm phải giữ thêm tính được cho phép của giao tiếp: Trong trường hợp thi hành một phương thức được đồng bộ hóa, khóa của đối tượng phải là tự do hoặc thuộc sở hữu của luồng gọi. Điều này được biểu diễn bởi   threadlockzthreadfreelockz  '.'. , trong đó thread là luồng gọi, z’ là đối tượng được gọi, và trong đó  lockzthread '. là thành phần đầu tiên của giá trị khóa, có nghĩa là, luồng đang sở hữu khóa của z’. Đối với sự thi hành của các phương thức điều phối ta yêu cầu rằng luồng đang thi hành - 53 - đang giữ khóa. Sự trả về từ phương thức wait giả thiết rằng luồng được thông báo và khóa của đối tượng được gọi là tự do. Định nghĩa 4.3.3. (Kiểm tra sự hợp tác: Giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với giao tiếp, nếu các điều kiện của định nghĩa 3.3.5 đúng đối với các lệnh được liệt kê ở đó với ngoại lệ của trường hợp quy tắc CALL, và thêm vào các trường hợp sau đây: 1.CALL: Sự thi hành của các phương thức không được đồng bộ hóa m với  notifyAllnotifywaitstartm ,,, được xử lý như trước đó. Đối với tất cả các lệnh       waitcallcallret peypemeup 3 ! 11 ! 201 :.:  (hoặc là các lệnh này mà không nhận một giá trị) trong lớp c với 0e của kiểu c’, trong đó phương thức  notifyAllnotifywaitstartm ,,, của c’ được đồng bộ hóa với thân     ret callcall ereturnstmqeyq ;: 3 ? 22 ? 2  , các biến hình thức u , và các biến cục bộ v ngoại trừ các biến hình thức, các điều kiện 2.6 và 2.7 phải đúng với các định nghía sau: Bất biến của lớp được gọi là '1 : cIq  . Khẳng định comm được cho bằng     threadlockzthreadfreelockzzzE  '.'.'0 . Hơn nữa, commf là    vInitzEvu ,:','  , 1obsf được cho bằng  zEyz 11 :.  , và 2obsf là  '':''. 22 zEyz  . 2. monitorCALL : Đối với  notifyAllnotifywaitm ,, , comm được cho bằng     threadlockzthreadzzE  '.'0 . 3. waitRETURN : Đối với      3 ! 33 ! 21 : qeyqreturnq retret getlock  trong phương thức wait, comm là     notifiedzthreadfreelockzzEuzzE '.''.''0  . Ví dụ 4.3.4. Giả thiết rằng sự thi hành của một phương thức được đồng bộ m của một lớp c, trong đó m của c có thân    returnstmthreadlockthreadstm call ;'?  . Chú ý rằng sự mở rộng được tích hợp trong stm thiết lập luồng sở hữu khóa bằng phép gán  lockinclock : . Kiểm tra sự hợp tác yêu cầu rằng       ''.'.:'.| threadlockzthreadlockzinclockztrueG  là đúng với định nghĩa của inc. - 54 - CHƯƠNG 5. PHÉP TOÁN ĐIỀU KIỆN TRƯỚC YẾU NHẤT Để tăng tính dễ đọc, kiểm chứng các điều kiện của các chương trước được đưa ra như là các bộ ba logic Hoare chuẩn. Mục đích của chúng ta là sử dụng một bộ chứng minh định lý để chứng minh các điều kiện này. Thay vì thi hành các ngữ nghĩa của các bộ ba logic Hoare trong bộ chứng minh định lý, ta đưa ra ngữ nghĩa trong các phép kéo theo logic thông qua một phép toán điều kiện trước yếu nhất. Theo cách này ta chỉ phải thi hành các ngữ nghĩa của các khẳng định trong bộ chứng minh định lý. 5.1. Các phép toán thay thế Sự thay thế cục bộ  yep / thay thế trong khẳng định cục bộ p tất cả các sự xuất hiện của các biến khác biệt y bằng các biểu thức cục bộ e . Ta cũng áp dụng sự thay thế cho các biểu thức cục bộ. Bổ đề sau biểu diễn thuộc tính chuẩn của sự thay thế ở trên, liên kết nó với cập nhật trạng thái. Quan hệ giữa sự thay thế và cập nhật được đưa ra trong bổ đề khẳng định rằng  yep / là điều kiện trước yếu nhất của p đối với phép gán ey : . Bổ đề được đưa ra cho các khẳng định, nhưng cùng thuộc tính đúng cho các biểu thức. Bổ đề 5.1.1. (Sự thay thế cục bộ) Đối với các môi trường logic  bất kỳ và các trạng thái thể hiện cục bộ   ,inst ta có  yepLinst /|,,  khi và chỉ khi         peyey LLLinst instinst |,, ,,,,    Sự kết quả của các phép gán được biểu diễn trong mức toàn cục bởi sự thay thế toàn cục  ezEP ./ , thay thế trong khẳng định toàn cục P các biến thể hiện x của đối tượng được tham chiếu tới bởi z bằng các biểu thức toàn cục E . Để có thể phù hợp với kết quả của các phép gán, ta phải không những thay thế theo cú pháp các xuất hiện của ixz. của các biến thể hiện, mà còn cho tất cả các bí danh của nó ixE '. , khi z và kết quả của sự thay thế được áp dụng cho E’ tham chiếu tới cùng đối tượng. Bởi vì điều kiện định danh không thể được kiểm tra theo cú pháp, ta định nghĩa trường hợp chính của sự thay thế bằng một biểu thức điều kiện      zxzEEifxzExE i  ./'./'. then iE else   ixxzEE ../' fi - 55 - Sự thay thế này được mở rộng cho các khẳng định toàn cục. Ta sử dụng sự thay thế  xzEP ./ cho dãy các biến bất kỳ y có thể chứa các biến logic, mà các ngữ nghĩa của chúng được định nghĩa bởi sự thay thế đồng thời  xzEx ./ và  uEu / , trong đó x và u là các dãy của các biến thể hiện và logic của y , các dãy con tương ứng xE và uE của E và  uEu / là sự thay thế như trong thay thế cục bộ; nếu chỉ các biến logic được thay thế, ta viết đơn giản  uEP / . Bổ đề 5.1.2. (Thay thế toàn cục) Đối với các trạng thái toàn cục  bất kỳ và các môi trường logic  chỉ tham chiếu tới các giá trị đang tồn tại trong  ta có  yzEPG ./|,  khi và chỉ khi PG|','  , trong đó     ,' GEy và        ,, .' GG Eyz  5.2. Kiểm chứng các điều kiện Trong kiểm chứng các điều kiện cục bộ, kết quả của một phép gán ey : được biểu diễn bởi sự thay thế e cho y trong các khẳng định. Trong các điều kiện toàn cục của kiểm tra sự hợp tác, kết quả của giao tiếp, chỉ thay đổi các trạng thái cục bộ, được biểu diễn bởi thay thế đồng thời các biến sẽ lưu trữ kết quả bằng các giá trị được giao tiếp. Điều đó có nghĩa là, đối với trường hợp lời gọi phương thức, các tham biến hình thức được thay thế bởi các tham biến thực được biểu diễn trong ngôn ngữ toàn cục. Kết quả của quan sát gọi call ey ! : trên một khẳng định toàn cục P được biểu diễn bằng sự thay thế   yzzEP ./ , trong đó z biểu diễn đối tượng gọi. Hiệu quả của quan sát được gọi được quản lý tương tự. Chú ý rằng thứ tự: đầu tiên giao tiếp diễn ra, được tiếp theo bởi quan sát gửi và sau đó là quan sát nhận. Để mô tả hiệu quả tách rời, đầu tiên ta phải thay thế đối với quan sát nhận, sau đó đối với quan sát nhận, và cuối cùng là đối với giao tiếp. Đối với một lời gọi phương thức, ta phải thêm vào thay thế đối với sự khởi tạo của các biến cục bộ. Để cho dễ đọc, trong các định nghĩa sau ta sử dụng ký hiệu fp với  yef / đối với sự thay thế  yep / ; ta sử dụng một ký hiệu tương tự cho các thay thế toàn cục. Chú ý rằng toán tử thay thế kết nối mạnh hơn các toán tử logic. - 56 - Định nghĩa 5.2.1. (Tính đúng đắn ban đầu) Một phác thảo chứng minh là đúng đắn ban đầu, nếu      ''.'| zznullzzzInitStateG        initobscinit ffzIzPGIfzP   32 . , trong đó c là lớp chính,     returnstmpeyp callcall ;: 3 ? 22 ? 2  là thân và các biến cục bộ v của phương thức run của c, cLVarz , và ObjectLVarz ' . Khẳng định toàn cục InitState được định nghĩa trước. Hơn nữa,      vvInitcallerthreadnullnullzf init /,/,0,, , và   22 ./ yzzEf obs  Định nghĩa 5.2.2. (Tính đúng đắn cục bộ: Phép gán) Một phác thảo chứng minh là đúng đắn cục bộ, nếu với tất cả các phép gán bội    21 : peyp  trong lớp c, không phải là quan sát của giao tiếp hoặc tạo đối tượng, asscL fpIp 21|  , với  yefass / . Định nghĩa 5.2.3. (Không có can thiệp) Một phác thảo chứng minh là không có can thiệp, nếu với tất cả các lớp c, và với tất cả các phép gán bội ey : với điều kiện trước p trong c, assccL fIIp | , với  yef ass / . Hơn nữa, đối với tất cả các khẳng định q tại các điểm điều khiển trong c, sao cho hoặc cả p và q không xuất hiện trong một phương thức được đồng bộ, hoặc q ở một điểm điều khiển đang chờ trả về,   asscL fqeIqp ':yq,interferes'|  . với khẳng định interferces như được định nghĩa ở phần trên. Định nghĩa 5.2.4. (Kiểm tra sự hợp tác: Giao tiếp) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với giao tiếp, nếu - 57 -          nullznullzcommzIzQzIzPGI ccG ''''| '11       commfzQzP ''22      commobsobs fffzQzPGI  1233 '' (5.5) là đúng đối với các biến logic mới khác biệt cLVarz và '' cLVarz  , trong các trường hợp sau: 1. (a) CALL: Đối với tất cả các lời gọi        waitcallcallret peypemeup 3 ! 11 ! 201 :.:  (hoặc các lời gọi không nhận một giá trị) trong lớp c với 0e thuộc kiểu 'c , trong đó phương thức  notifyAllnotifywaitstartm ,,, của c’ được đồng bộ hóa với thân     ret callcall ereturnstmqeyq ;: 3 ? 22 ? 2  , các tham biến hình thức u , và các biến cục bộ v trừ các tham biến hình thức. Bất biến của lớp được gọi là '1 cIq  . Khẳng định comm được cho bằng     threadlockzthreadfreelockzzzE  '.'.'0 . Hơn nữa,     ','/, vuvInitzEfcomm ,   111 ./ yzzEfobs  ,   222 './'' yzzEfobs  . Nếu m không được đồng bộ hóa,   threadlockzthreadfreelockz  '.'. trong comm được loại bỏ. (b) monitorCALL : Với  notifyAllnotifywaitm ,, , comm được cho bằng     threadlockzthreadzzE  '.'0 . (c) startCALL : Với m = start, comm là   startedzzzE '.'0  , trong đó     returnstmqeyq callcall ;: 3 ? 22 ? 2  là thân của phương thức run của c’. (d) skipstartCALL : Với m = start, thêm vào, (5.5) phải là đúng với comm được cho bằng   startedzzzE '.'0  , trueqq  32 , và commf và 2obsf là định danh các hàm. 2. (a) RETURN : Đối với tất các lệnh gọi phương thức        3 ? 44 ? 21 ! 110 ::.: peyppeyemeu retretwaitcall ret  (hoặc các lệnh này mà không nhận một giá trị) xuất hiện trong c với 0e của kiểu c’, sao cho - 58 - phương thức  um của c’ có lệnh trả về      3 ! 33 ! 21 : qeyqereturnq retret ret , phương trình (5.5) phải là đúng với comm được cho bằng    zEuzzE  ''0 , và trong đó   retretcomm uzEf /'' ,   331 ''./'' yzzEfobs  , và   442 ./ yzzEfobs  . (b) waitRETURN : Với      3 ! 33 ! 21 : qeyqreturnq retret getlock  trong phương thức wait, comm là     notifiedzthreadfreelockzzEuzzE '.''.''0  . (c) runRETURN : Với      3 ! 33 ! 21 : qeyqreturnq retret  xuất hiện trong phương thức run, trueppp  321 , comm = true, và hơn nữa commf và 2obsf là định danh các hàm. Định nghĩa 5.2.5. (Kiểm tra sự hợp tác: Tạo đối tượng) Một phác thảo chứng minh thỏa mãn kiểm tra sự hợp tác đối với tạo đối tượng, nếu với tất cả các lớp c’ và các lệnh      321 :: peypnewup newnewc  trong c’:          '.,''.| '1 zzIzPuGIuzFreshzuznullz cG        obsfzPGIuzP 3c2 I  , với 'cLVarz và listObjectLVarz ' là đối tượng mới,   yzzEfobs ./ , và Fresh và  được định nghĩa ở trong 2.4.2. - 59 - CHƯƠNG 6. TÍNH ĐÚNG ĐẮN Một chương trình được cho cùng với chú thích của nó, hệ chứng minh quy định một số kiểm chứng các điều kiện đối với các kiểu khác nhau của các khẳng định và các cấu trúc chương trình. Tính đúng đắn của hệ chứng minh có nghĩa là đối với một phác thảo chứng minh thỏa mãn kiểm chứng các điều kiện, tất cả các cấu hình có thể đạt được trong các ngữ nghĩa của toán tử thỏa mãn các khẳng định được cho. Để thuận tiện, ta giới thiệu các chú thích sau: Một chương trình được cho prog, ta viết prog hoặc  cho chú thích của nó, và viết |prog , nếu prog thỏa mãn tất cả các yêu cầu được phát biểu trong các khẳng định, và '|' prog , nếu prog’ với chú thích ' thỏa mãn kiểm chứng các điều kiện của hệ chứng minh: Định nghĩa 6.0.1. Một chương trình được cho prog với chú thích  , thì |prog khi và chỉ khi với tất cả các cấu hình có thể đạt được ,T của prog, với tất cả   Tstm ,,  , và với tất cả các môi trường logic  chỉ tham chiếu tới các giá trị đang tồn tại trong  : 1.    stmpreL|,,  , và 2. GIG|, . Hơn nữa, với tất cả các lớp c, các đối tượng   cVal , và các trạng thái cục bộ ' : 3.   cL I|',,  . Đối với các phác thảo chứng minh, ta viết '|' prog khi và chỉ khi prog’ với chú thích ' thỏa mãn kiểm chứng các điều kiện của hệ chứng minh. 6.1. Tính đúng đắn Tính đúng đắn có nghĩa là tất cả các cấu hình có thể đạt được thỏa mãn các khẳng định của chúng đối với một chương trình được chú thích – được kiểm chứng bằng sử dụng chứng minh các điều kiện. Tính đúng đắn của một phương thức được chứng minh bằng một quy nạp đơn giản trong số của các bước tính toán. - 60 - Trước khi bắt tay vào trình bày tính đúng đắn và chứng minh của nó, ta cần hiểu rõ mối quan hệ giữa chương trình gốc và phác thảo chứng minh, có nghĩa là, chương trình gốc được mở rộng bằng các biến phụ trợ, và được bao bọc với các khẳng định. Để tạo sự rõ ràng trong mối quan hệ giữa chương trình gốc và phác thảo chứng minh, ta định nghĩa một toán tử chiếu prog , xóa tất cả các phần thêm vào của sự biến đổi. Cho prog’ là một phác thảo chứng minh với prog, và ',' T là một cấu hình toàn cục của prog’. Thì prog' được định nghĩa bởi bỏ đi tất cả các biến thể hiện phụ trợ từ các miền trạng thái thể hiện. Với tập các cấu hình luồng, progT ' được cho bởi hạn chế các miền của các trạng thái cục bộ để không có các biến phụ trợ và bỏ đi tất cả các bổ sung. Thêm vào đó, với các cấu hình cục bộ   ',, ! Tstmreturn retgetlock  , nếu luồng đang thi hành ở trong tập đợi, nghĩa là, nếu      waitnthread  ',  với một số n nào đó, thì lệnh getlockreturn được thay thế bằng getlockreturnsignal;? . Hơn nữa, với các cấu hình cục bộ   '';,, ! Tstmreturnstm ret  với stm một phép gán phụ trợ trong phương thức notify hoặc trong phương thức notifyAll, phép gán phụ trợ stm được thay thế theo thứ tự bằng !signal và !signal_all. Bổ đề sau biểu thị rằng nếu sự biến đổi không thay đổi hành vi của các chương trình: Bổ đề 6.1.1. Cho prog’ là một phác thảo chứng minh với một chương trình prog. Thì ,T là một cấu hình có thể đạt được của prog khi và chỉ khi tồn tại một cấu hình có thể đạt được ',' T của prog’ với  ,',' TprogprogT  . Bổ đề 6.1.2. (Định danh) Cho ,T là một cấu hình có thể đạt được của một phác thảo chứng minh. Thì: 1. với tất cả các ngăn xếp  và ' trong T và với tất cả các cấu hình cục bộ    stm,, và   '',','  stm ta có    threadthread '  khi và chỉ khi '  , và 2. với mỗi ngăn xếp    nnn stmstm ,,...,, 000  trong T và các chỉ số nji  ,0 , (a)   0 threadi ; (b) i < j và ji   kéo theo       counterconfconf iji   , (c) 0 < j kéo theo       threadconfcaller jjjj 111 ,,   , và (d)     threadcallerproj 00 3,   , - 61 - trong đó  ivproj , là thành phần thứ i của bộ v. Bổ đề sau phát biểu rằng luồng sở hữu khóa, và các tập đợi và tập được thông báo của các ngữ nghĩa được trình bày bởi các biến lock, wait, và notified. Hơn nữa, bổ đề đảm bảo rằng tính phân đoạn của các dãy được lưu trữ trong các biến wait và notified; nếu thứ tự của các phần tử không quan trọng, ta sử dụng tập ký hiệu cho các giá trị của chúng. Bổ đề 6.1.3. (Lock, Wait, Notify) Cho ,T là một cấu hình có thể đạt được của một phác thảo chứng minh với chương trình gốc prog,   Val là một định danh đối tượng, và cho   Tstm  ',, 000   . Hơn nữa cho n là số của các thi hành phương được đồng bộ của  trong  , nghĩa là, n =   |.|,,| synchrstmstm   . Thì: 1. (a)  ,progTowns  khi và chỉ khi    freelock  (b)   ,progowns  khi và chỉ khi     nlock ,0  2. (a)   ,progTwait  khi và chỉ khi     waitn  ,0 (b)   ,progTnotified  khi và chỉ khi     notifiedn  ,0 (c)     1,iwaitproj  =     1,jwaitproj  kéo theo i = j (d)     1,inotifiedproj  =     1,jnoitifiedproj  kéo theo i = j (e) nếu     waitm  ,0 hoặc     notifiedm  ,0 thì m = n (f)      notifiedwait    trong đó  is là thành phần thứ i của dãy s. Cuối cùng, biến thể hiện phụ trợ started của một đối tượng lưu trữ nếu luồng của đối tượng đã được khởi động hoặc không: Bổ đề 6.1.4. (Started) Đối với tất cả các cấu hình có thể đạt được ,T của một phác thảo chứng minh cho một chương trình prog, và tất cả các đối tượng   Val , ta có  ,progTstarted  khi và chỉ khi   started . Cho prog là một chương trình với chú thích  , và prog’ một phác thảo chứng minh tương ứng với chú thích ' . Cho GI’ là bất biến toàn cục của ' , 'cI biểu thị các - 62 - bất biến lớp của nó, và với một khẳng định p của  cho p’ biểu thị khẳng định của ' được kết hợp với cùng điểm điều khiển. Ta viết '|  khi và chỉ khi GIGIG  '| , ccL II  '| đối với tất cả các lớp c, và '| ppL  , đối với tất cả các khẳng định p của  được kết hợp với các điểm điều khiển nào đó. Để cho các biến phụ trợ ngữ nghĩa, các kéo theo ở trên được ước lượng trong ngữ cảnh của các trạng thái của chương trình được bổ sung. Định lý sau phát biểu tính đúng đắn của phương pháp chứng minh. Định lý 6.1.5. (Tính đúng đắn) Cho prog’ là một phác thảo chứng minh với chú thích 'prog . Nếu '|' progprog  thì '|' progprog  Chứng minh tính đúng đắn bao gồm một chứng minh quy nạp trong chiều dài của tính toán, đồng thời trong tất cả ba phần từ định nghĩa 6.0.1. Đối với bước quy nạp, ta giả thiết rằng kiểm chứng các điều kiện được thỏa mãn và giả thiết một cấu hình có thể đạt được thỏa mãn chú thích. Ta tạo trường hợp khác biệt trong cú pháp của bước tính toán kế tiếp: Nếu bước tính toán thi hành một phép gán, thì ta sử dụng các điều kiện tính đúng đắn cục bộ để chứng minh tính quy nạp của sự thi hành các thuộc tính của cấu hình cục bộ, và kiểm tra tính không có can thiệp đối với tất cả các cấu hình cục bộ khác và các bất biến lớp khác. Đối với giao tiếp, tính bất biến đối với thi hành các đối tác và bất biến toàn cục được chứng tỏ bằng sử dụng kiểm tra sự hợp tác đối với giao tiếp. Giao tiếp với chính nó không ảnh hưởng trạng thái toàn cục; tính bất biến của các thuộc tính còn lại dưới các quan sát tương ứng được chứng tỏ với sự giúp đỡ của của kiểm tra tính không có can thiệp. Cuối cùng, đối với tạo đối tượng, tính bất biến đối với bất biến toàn cục, tạo cấu hình cục bộ, bất biến lớp của đối tượng được tạo được đảm bảo các điều kiện của kiểm tra hợp tác đối với tạo đối tượng; tất cả các thuộc tính khác được chứng tỏ là bất biến thông qua sử dụng kiểm tra tính không có can thiệp. Định lý 6.1.5 được đưa ra đối với tính có thể đạt được của các chương trình được bổ sung. Với sự giúp đỡ của bổ đề 6.1.1, ta có ngay lập tức : Hệ quả 6.1.6. Nếu '|' progprog  và progprog   '| , thì progprog | . - 63 - KẾT LUẬN Với sự phát triển không ngừng của nhu cầu tính toán, xử lý số liệu, khai phá thông tin thì lập trình đa luồng ngày càng quan trọng và là một phần không thể thiếu trong các hệ thống tính toán, cũng như trong các hệ thống ứng dụng. Sự quan trọng và cần thiết của việc kiểm chứng tính đúng của chương trình luôn được quan tâm đúng mức do vai trò to lớn của nó. Kiểm chứng tính đúng đắn của chương trình Java đa luồng không chỉ mang ý nghĩa về mặt lý thuyết của kiểm chứng mà nó thực sự có vai trò không thể thiếu trong thực tế, qua đó giúp ta tránh được những sai lầm, thiếu sót dù là rất nhỏ nhưng có thể dẫn tới những hậu quả thật khó lường. Trong các hệ thống đòi hỏi tính an toàn cao như các hệ thời gian thực, các hệ mô phỏng, hoặc các hệ thống giám sát vệ tinh, máy bay thì kiểm chứng tính đúng đắn của các chương trình mang một ý nghĩa vô cùng to lớn. Nó cho phép xác định được tính đúng đắn của chương trình từ các giả thiết và các khẳng định ban đầu mà không cần phải chứng thực điều đó khi chạy chương trình, mà nếu trong thực tế chương trình chạy sai gây ra hậu quả vô cùng nghiêm trọng. Phương pháp kiểm chứng trên còn được sử dụng để chứng minh tính không có deadlock của một chương trình Java. Phác thảo chứng minh của chương trình nếu thỏa mãn các điều kiện của chứng minh tính không có deadlock thì chương trình sẽ không có deadlock. Để có thể kiểm chứng tính đúng đắn của một chương trình Java đa luồng, ta có thể sử dụng phương pháp đã trình bày ở trên. Nó là cơ sở, tiền đề để xây dựng các công cụ hỗ trợ việc kiểm chứng tự động. Do thời gian thực hiện đề tài có hạn và phạm vi rộng lớn của đề tài, khóa luận chưa đề cập hết được các phương pháp cũng như kỹ thuật hiện đại kiểm chứng tính đúng đắn của chương trình, cũng như các công cụ hỗ trợ kiểm chứng hiện nay. - 64 - TÀI LIỆU THAM KHẢO [1] Erika Abraham - An Assertional Proof System for Multitheaded Java – Theory and Tool Support WEBSITE: [2] [3]