Ngữ nghĩa CSP cho các mạch tuần tự không đồng bộ

Nội dung text: Ngữ nghĩa CSP cho các mạch tuần tự không đồng bộ

1. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải NGỮ NGHĨA CSP CHO CÁC MẠCH TUẦN TỰ KHÔNG ĐỒNG BỘ Trần Văn Dũng Trường Đại học Giao thông Vận tải, Số 3 Cầu Giấy, Hà Nội Email: zungtv@yahoo.com; Tel: 0904588833 Tóm tắt. Bài báo sử dụng công cụ đại số “Các tiến trình tuần tự tương tác CSP”– Communicating Sequential Processes của C.A.R. Hoare [1] để xây dựng các chương trình tuần tự không đồng bộ mô phỏng các mạch tuần tự không đồng bộ và đưa ra phương pháp mô phỏng dựa trên các luật của đại số CSP và các luật logic để chứng minh các tính chất của một số chương trình tuần tự không đồng bộ. Từ khóa: tiến trình tuần tự tương tác CSP, mạch tuần tự không đồng bộ, chương trình tuần tự không đồng bộ. 1. ĐẶT VẤN ĐỀ Mục đích của bài báo nhằm đưa ra cách tiếp cận sử dụng đại số các tiến trình tuần tự tương tác CSP để xây dựng các tiến trình mô phỏng hoạt động của các mạch tuần tự không đồng bộ, tức là mạch xử lý thông tin mà ngoài đầu vào và đầu ra có thể cho phép quay vòng một số thông tin bên trong mạch và hoạt động theo các chu kỳ kích hoạt đầu vào không sử dụng đồng hồ đồng bộ. Các mạch tuần tự không đồng bộ là một loại mạch phần cứng quan trọng, chính vì vậy việc tìm hiểu và suy luận về các hành vi của mạch có ý nghĩa quan trọng và thu hút sự quan tâm nghiên cứu của nhiều tác giả (xem [2,3,4]). Bên cạnh công cụ CSP, trong [5] chúng ta đã sử dụng mô hình toán học khác để nghiên cứu việc tích hợp không đồng bộ các tiến trình tuần tự. Trong bài này ta xét mạch tuần tự không đồng bộ theo trình tự các bước như sau: • Bổ sung biến delay vào các vị trị cần thiết, trước khi quay vòng • Biểu diễn các biến bổ sung thông qua đầu vào, đầu ra và thông tin quay vòng • Tìm mối liên hệ giữa các biến xem có thoả mãn các điều kiện cần thiết không • Xét mạch hoạt động có cho kết quả duy nhất không, tức là thiết kế tốt không? Ở đây ta xét chế độ thao tác cơ bản mở rộng theo nghĩa sau: các tín hiệu vào có thể đồng bộ thay đổi, nhưng sau đó mọi tín hiệu vào khác chờ đợi cho đến khi mạch đạt đến trạng thái cân bằng tiếp theo, tức là khi mọi biến không thay đổi giá trị nữa. Khi ghép nối các mạch, nếu các mạch thành phần là lũy đẳng, tức là nếu thực hiện thêm một lần thứ hai nữa, thì không đem lại kết quả gì mới hoặc bản thân nó là mạch tổ hợp, thì nguyên tắc hoạt động trên luôn được đảm bảo. 2. CÁC MẠCH TUẦN TỰ KHÔNG ĐỒNG BỘ. Chúng ta sẽ dùng khái niệm chương trình tuần tự không đồng bộ để mô phỏng hoạt động của mạch không đồng bộ. Trong mạch có thể có nhiều luồng thành phần, -267-
2. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải chúng thay nhau thực hiện một cách tùy ý, cho đến khi mọi việc thực hiện sẽ không đem lại kết quả gì mới nữa. Lúc đó ta nói mạch ở trạng thái ổn định và dừng. Chúng ta mong muốn tìm hiểu các điều kiện ràng buộc đối với các mạch mà kết quả cuối cùng khi thực hiện chúng là tất định, không phụ thuộc vào thứ tự thực hiện tùy chọn của các luồng [2]. Ví dụ 1. Cho mạch tuần tự không đồng bộ trên Hình 1 sau: Hình 1. Mạch không đồng bộ đơn giản Ở đây có hai đầu vào S, R và một đầu ra Q với một biến bên trong X. Hai biến X, Q gắn với hai mạch NOT OR, ta bổ sung biến delay Q* cho Q trước khi quay về, nếu thấy cần thiết trong suy luận hoạt động của mạch. Vậy ta có hai phương trình sau: X = S’• Q’ (1) Q = X’ • R’ Ở đây để đơn giản ký hiệu A’ là phủ định của A và • là phép hội logic hai mệnh đề. Ở đây ta đồng nhất Q* và Q và xét như một chương trình đệ qui. Vấn đề đặt ra là tìm cách tiếp cận để mô phỏng hoạt động của mạch bằng một chương trình song song không đồng bộ, mà sẽ xét ở mục sau. 3. ĐẠI SỐ CÁC TIẾN TRÌNH TUẦN TỰ TƯƠNG TÁC CSP Năm 1984, C.A.R. Hoare [1] đã xây dựng lý thuyết đại số các tiến trình tương tác CSP. Đó là một cách tiếp cận hình thức dựa trên logic để mô phỏng hoạt động của các hệ thống gồm các tiến trình song song và tương tác lẫn nhau. Từ đó trở đi CSP đã trở thành một trong những mô hình toán học quan trọng để thiết kế và suy luận về lập trình song song. Sau đây chúng ta trình bày một số định nghĩa và các luật cơ bản của CSP [1]. • Tiến trình. Giả sử P là một tiến trình, ta ký hiệu P là bảng chữ gồm các sự kiện của P. Tiến trình được xét ở đây là một khái niệm trừu tượng tuân theo các luật cơ bản của CSP mà sẽ được bổ sung dần qua quá trình phát triển sau. • Prefix. Giả sử P là một tiến trình và a là một sự kiện thuộc P, Khi đó (a → P) là một tiến trình mà trước hết a xảy ra sau đó đến tiến trình P. • Đệ qui. Một tiến trình có thể được mô tả qua chính nó. Ví dụ máy tự động Q bỏ đồng xu sẽ cho ra lon coca được mô tả như sau: Q = xu → coca → Q. Đôi khi ta ký hiệu là Q = μ X ● (xu→ coca → X), trong đó μ X ● F(X) là điểm bất động cực đại của hàm F(X). • Lựa chọn. Giả sử P, Q là hai tiến trình và a, b là hai sự kiện. Khi đó (a → P | b → Q) là tiến trình ban đầu có thể tùy chọn a hoặc b và nếu a xảy ra thì sau đó nối tiếp bởi P, còn nếu b xảy ra thì được nối tiếp bằng Q. Ví dụ máy tự động bỏ xu nhỏ cho -268-
3. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải chocola, bỏ xu to cho coca được mô tả Q = (xu_nho → chocola → Q | xu_to → coca →Q). Ta có thể dùng ký hiệu tổng quát hơn (x:A → P(x)), nghĩa là đây là một tiến trình mà khi x được xác định là sự kiện đầu trong tập A, thì sẽ được nối tiếp bởi tiến trình P(x). • Phép toán không tất định. Giả sử P, Q là hai tiến trình. Khi đó P ᴨ Q là tiến trình mà có hành vi giống P hoặc Q, ở đó việc lựa chọn giữa chúng là tùy ý, không có kiến thức gì về môi trường xung quanh. • Tùy chọn tổng quát. Giả sử P, Q là hai tiến trình. Khi đó P  Q là tiến trình có hành vi giống P hoặc giống Q, ở đó việc lựa chọn giữa P và Q là có điều khiển dựa trên các sự kiện ban đầu của P và Q. Nếu sự kiện ban đầu của P là không thể, thì Q được chọn, nếu Q không thể tiến hành từ đầu, thì P được chọn. Nếu cả hai sự kiện đầu của P và Q đều có thể, thì việc lựa chọn giữa P và Q là tùy ý. Ta có hai luật sau: (c → P  d → Q) = (c → P | d → Q), nếu c d (2) (c → P  c → Q) = (c → P ᴨ c → Q) (3) • Phép toán song song. Giả sử P và Q là hai tiến trình có hai bảng chữ khác nhau, tuy nhiên vẫn có thể có các phần tử chung của hai bảng chữ đó. Ta định nghĩa phép toán song song || của hai tiến trình P và Q như sau: (P||Q) = P  Q Giả sử a є P- Q, b є Q- P và c, d є P Q. Ta có các luật của phép toán song song || như sau: (c → P || c → Q) = (c → (P || Q)), (4) (c → P || d → Q) = STOP, nếu c d (5) (a → P || c → Q) = (a→ (P || c→ Q), (6) (c → P || b → Q) = (b → (c→ P || Q), (7) (a → P || b → Q) = (a → (P||(b→ Q))|(b → (a → P||Q)), (8) • Phép toán che giấu. Giả sử P là một tiến trình và C là một tập các sự kiện. Khi đó tiến trình nhận được từ P bằng cách che giấu các sự kiện trong C được ký hiệu là P\C với (P\C)= (P)\C. Các dãy sự kiện của P\C nhận được từ dãy sự kiện của P bỏ đi các sự kiện trong C. 4. SỬ DỤNG CSP MÔ PHỎNG CÁC MẠCH TUẦN TỰ KHÔNG ĐỒNG BỘ. Trước hết chúng ta thử tìm cách dùng khái niệm tiến trình từ tố trong [1] để mô tả các thành phần X và Q trong Ví dụ 1 ở mục 2 như chúng ta đã thử làm trong [4], nhưng ở đây chúng ta sử dụng cách tiếp cận khác. Hai phương trình (1) trên đều có dạng giống nhau đều mô phỏng mạch NOT OR. Xét phương trình thứ nhất, ta có một số nhận xét sau: • Giá trị x chỉ thay đổi khi ít nhất một trong hai giá trị của s hoặc q thay đổi. • Khi đầu vào s thay đổi sẽ kích hoạt mạch thứ nhất hoạt động và thực hiện sự kiện x. Tuy nhiên khi sau khi thực hiện x, có hai khả năng xảy ra -269-
4. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải o Giá trị x không thay đổi, coi như không thực hiện hành động nào o Giá trị x thay đổi và kích hoạt sự kiện ~x ghi nhận sự thay đổi của x. Xét các tiến trình I, X, Q với bảng chữ tương ứng được định nghĩa như sau: α(I) = {~s, ~r}; α(X) = {~s, x, ~x ,⌐~x, ~q}. I = ~s → I | ~r → I X = (~s → x → ⌐~x → X) | (~s → x → ~x → X) | (~q → x → ⌐~x → X) | (~q → x → ~x → X) α(Q) = {~r, q, ~q ,⌐~q, ~x}. Q = (~r → q → ⌐~q → Q) | (~r → q → ~q → Q) | (~x → q → ⌐~q → Q) | (~x → q → ~q → Q) Chẳng hạn, khi s thay đổi, tập các hành vi có thể của tiến trình I || X || Q có thể được sinh ra dựa trên các luật của CSP (3-4-5-7) như sau: I || X || Q = ~s → I || X || Q = ~s → I || (~s → x → (⌐~x→ X | ~x → X)) || Q = ~s → (I || x → (⌐~x→ X | ~x → X) || Q) = ~s → x → (I ||(⌐~x → X □ ~x→ X) || Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → (I || ~x→ X || Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → (I || ~x→ X || ~x → q →(⌐~q→ Q | ~q → Q)) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q → (I ||X ||(⌐~q→ Q | ~q → Q)) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q→ ⌐~q→ (I ||X ||Q) □ ~s → x → ~x → q → (I ||X ||~q→ Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q→ ⌐~q→ (I ||X ||Q) □ ~s → x → ~x → q → (I ||~q→ x→(⌐~x→ X | ~x → X) ||~q→Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q→ ⌐~q→ (I ||X ||Q) □ ~s → x → ~x → q → ~q→ x→ (I ||(⌐~x→ X | ~x → X) ||Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q→ ⌐~q→ (I ||X ||Q) □ ~s → x → ~x → q → ~q→ x→ ⌐~x→ (I ||X ||Q) □ ~s → x → ~x → q → ~q→ x→ ~x→ q →(I ||X ||(⌐~q→ Q | ~q → Q) = ~s → x → ⌐~x → (I || X || Q) □ ~s → x → ~x → q→ ⌐~q→ (I ||X ||Q) □ ~s → x → ~x → q → ~q→ x→ ⌐~x→ (I ||X ||Q) □ ~s → x → ~x → q → ~q→ x→ ~x→ q → ⌐~q→ (I ||X ||Q) Lưu ý ở duy diễn cuối ta chỉ áp dụng Q = ~x → q → ⌐~q → Q, vì khả năng trong bối cảnh ~s → x → ~x → q → ~q→ x→ ~x→ q, giá trị q không thay đổi do quan hệ X;Q;X;Q là lũy đẳng. Thực vậy dễ dàng thấy: X;Q = {X = S’•Q’} Q -270-
5. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải = {X = S’•Q’} (X’•R’) = (S’•Q’)’•R’ = (S + Q)•R’ = S•R’ + Q•R’ X;Q;X;Q = {X|S’•Q’}(Q = X’•R’); X; Q = {Q|S•R’ + Q•R’}(X = S’• Q’);Q = {X|S’•(S•R’ + Q•R’)’} Q = {X|S’•(S•R’ + Q•R’)’} (Q = X’•R’) = (S’•(S•R’ + Q•R’)’)’•R’ = (S + (S•R’ + Q•R’))•R’ = (S + Q•R’)•R’ = S•R’ + Q•R’ = X;Q Do đó X;Q là chương trình lũy đẳng. Xét tương tự khi cho r thay đổi giá trị và kích hoạt mạch ở trạng thái ổn định hoặc khi cả s và r đồng thời thay đổi giá trị. Do đó chúng ta nhận được kết quả sau, khi che giấu các hành động thay đổi giá trị bên trong: (I || X || Q) \ {~x,⌐~x,~q,⌐~q} = μ(Y)• (~s→ x→ q □ ~r→ q→ x)→ Y) = ~s→ x→ q □ ~r→ q→ x Một hành vi đúng là một dãy các sự kiện theo khuôn mẫu trên. Ví dụ xuất phát từ trạng thái ổn định: rsxq = 0001, tức là r = 0, s = 0, x = 0, q = 1 và các phương trình trong 1 đều thỏa mãn: 0’• 1’ = 1 • 0 = 0 0’• 0’ = 1 • 1 = 1 Bây giờ ta cho s tăng từ 0 lên 1, ta có hành vi đúng sau: s = 1 → x = = 1’• 0’ = 0 → ⌐~x Sau khi chạy chương trình I || X || Q, ta nhận được r = 0, s =1, x = 0, q = 1, tức là nó sẽ chuyển về trạng thái 0101. Giả sử bây giờ xuất phát từ trạng thái ổn định: rsxq = 0100, bây giờ ta cho s giảm từ 1 về 0, ta có hành vi đúng sau: s = 0 → x = 0’• 0’ = 1 → ~x → q = 1’• 0’ = 0 → ⌐~q Sau khi chạy chương trình I || X || Q nó sẽ chuyển về trạng thái 0010. Giả sử bây giờ xuất phát từ trạng thái ổn định: rsxq = 1100, bây giờ ta cho r giảm từ 1 về 0, ta có hành vi đúng sau: r = 0 → q = 1 → ~q → x = 0 → ⌐~x Sau khi chạy chương trình I || X || Q nó sẽ chuyển về trạng thái 0101. Như vậy chúng ta có thể dựa trên mô hình CSP để suy luận về hoạt động của mạch. Trong phần sau chúng ta sẽ đưa ra các bước cụ thể của phương pháp mô hình hóa. -271-
6. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải 5. PHƯƠNG PHÁP MÔ HÌNH HÓA Qua các ví dụ trên, chúng ta thấy, một mạch tuần tự không đồng bộ bất kỳ được mô phỏng bằng một chương trình gọi là không đồng bộ là dạng kết hợp song song các chương trình mà là chương trình tuần tự hoặc chương trình không đồng bộ dừng. Do đó, dựa trên những nhận xét đưa ra khi xét Ví dụ 1, chúng ta khái quát các nguyên tắc mô phỏng một mạch tuần tự không đồng bộ bằng đại số CSP như sau: Các nguyên tắc mô phỏng: • Mỗi đường ra từ một mạch quay lui ký hiệu một chương trình tuần tự. Một số mạch cùng có chung đầu vào và khép kín mạch quay lui tạo nên một mạch tuần tự không đồng bộ cơ sở. • Mạch tuần tự không đồng bộ cơ sở sẽ hoạt động từ việc kích hoạt thay đổi một đầu vào, kích hoạt các mạch thành phần hoạt động, tương tác qua lại với nhau, cho đến khi đạt được một trạng thái ổn định và dừng lại chờ chu kỳ tiếp theo. • Mạch tuần tự không đồng bộ được mô phỏng bằng một chương trình tuần tự không đồng bộ là một tiến trình khung gồm nhiều tiến trình thành phần kết nối song song với nhau, các tiến trình thành phần là các chương trình tuần tự hoặc các chương trình tuần tự không đồng bộ dừng. • Việc mô phỏng trên chỉ phụ thuộc vào các đầu vào và trạng thái của chương trình. Các biến đầu vào và các biến quay lui loan báo sự thay đổi giá trị và đồng bộ sự thay đổi của các biến ở các tiến trình thành phần. Tiến trình không đồng bộ nhận được gọi là tiến trình khung. • Một thực thi của chương trình là một cách lựa chọn cú pháp của chương trình phù hợp với việc thay đổi trạng thái trung gian của mạch. Một chương trình không đồng bộ thiết kế tốt là chương trình mà mọi thực thi có thể đều dẫn đến trạng thái ổn định như nhau. • Hướng tới việc đảm bảo qui tắc trên, ta bổ sung một số qui tắc đảm bảo tính giao hoán của các sự kiện biến tính thay đổi và tính lũy đẳng của mỗi sự kiện biến tính thay đổi, hay tính đơn vị trái nửa giao hoán của biến không đổi. • Như vậy một chương trình khung tuần tự không đồng bộ được xây dựng đại diện cho một tập các mạch tuần tự không đồng bộ có cùng cấu trúc. Dựa vào chương trình khung và phương trình các mạch thành phần chúng ta sẽ bổ sung các luật đặc tả cho các biểu thức logic bên trong của các mạch tuần tự không đồng bộ cụ thể. Ví dụ 2. Cho mạch tuần tự không đồng bộ trên Hình 2 sau. Ngoài hai biến đầu vào X, Y và biến đầu ra Z, ta bổ sung hai biến trong P, Q với thời gian delay không xác định. Vì P, Q, Z có quay lui, nên ta coi P, Q, Z là các chương trình luồng thành phần. Như vậy mỗi bộ giá trị của các biến (P, Q, X, Y, Z) sẽ xác định một trạng thái của chương trình. Ta có thể coi mạch trên là kết nối song song của ba mạch thành phần như sau: -272-
7. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải Hình 2. Mạch không đồng bộ phức tạp Có thể mô tả các trạng thái của mạng qua otomat chuyển trạng thái bên trong PQ, với đầu vào XY và đầu ra Z bằng otomat sau: Hình 3. Otomat chuyển trạng thái của mạch trên Hình 2 Tuy nhiên ở đây, chúng ta muốn mô phỏng mạch bằng chương trình tuần tự không đồng bộ. Xét các phương trình: Q = Y’•Q + X (9) P = P•Q + P•Y + Y’•X’•Q Z = P•X + Q’•Y Lưu ý Z, P và Q đều là lũy đẳng. Do đó sau lần thứ hai thực hiện các chương trình trên các biến sẽ không thay đổi giá trị nữa. Ta mô phỏng mạch trên bằng tiến trình CSP: α(I) = {~x, ~y, ~xq, ~yq, ~xp, ~yp}. α(Q) = {~xq, ~yq, ~yq, q, ~qq, ~qp, ~qz,⌐~q}. α(P) = {~xp, ~yp, ~qp, ~yp, ~pp, ~pz , ⌐~p}. α(Z) = {~xz, ~yz, ~qz, ~pz} -273-
8. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải I = ~x → (~xi→ ~xj→ ~xk)→ I | ~y → (~yi→ ~yj→ ~yk)→ I Q = (~xq □ ~yq □ ~qq ) → q → ((~qi→ ~qj→ ~qk ) □ ⌐~q) → Q Với (i, j, k) là hoán vị bất kỳ của (q, p, z), ta có: P = (~xp □ ~yp □ ~qp □ ~pp)→ p → ((~pl→ ~pt ) □ ⌐~p) → P Với (l, t) là hoán vị bất kỳ của (p, z), ta có: Z = (~xp □ ~yp □ ~qz □ ~pz)→ z→ Z I || Q || P || Z = (~x → (~xi→ ~xj→ ~xk)→ I |~y → (~xi→ ~xj→ ~xk)→ I) || Q || P || Z Xét một hành vi của mạch ~x → (~xq→ ~xp→ ~xz)→ I) || Q || P || Z = ~x → (~xq → ~xp→ ~xz → I) || ~xq → q→ ⌐~q → Q || P || Z) = ~x → ~xq → (~xp→ ~xz → I || q→ ⌐~q → Q || P || Z) = ~x → ~xq → q → (~xp→ ~xz → I ||⌐~q → Q || P || Z) = ~x → ~xq → q →⌐~q → (~xp→ ~xz → I || Q || P || Z) = ~x → ~xq → q→ ⌐~q → ~xp→(~xz → I || Q || p→ ⌐~p→ P || Z) = ~x → ~xq → q→ ⌐~q → ~xp→ p→ (~xz → I || Q ||⌐~p→ P || Z) = ~x → ~xq → q→ ⌐~q → ~xp→ p→(~xz → I || Q ||P || Z) = ~x → ~xq → q→ ⌐~q → ~xp→ p→(~xz → I || Q ||P ||~xz→ z→ Z) = ~x → ~xq → q→ ⌐~q → ~xp→ p→ ~xz →(I || Q ||P || z→ Z) = ~x → ~xq → q→ ⌐~q → ~xp→ p→ ~xz → z→ (I || Q || P || Z) Và một hành vi khác ~y → (~yq→ ~yp→ ~yz)→ I) || Q || P || Z = ~y → (~yq → ~yp→ ~yz → I) || ~yq → q→ ⌐~q → Q || P || Z) = ~y → ~yq → (~yp→ ~yz → I || q→ ⌐~q → Q || P || Z) = ~y → ~yq → q → (~yp→ ~yz → I ||⌐~q → Q || P || Z) = ~y → ~yq → q → ⌐~q → (~yp→ ~yz → I || Q || P || Z) = ~y → ~yq → q→ ⌐~q → ~yp→(~yz → I || Q || p→ ⌐~p→ P || Z) = ~y → ~yq → q→ ⌐~q → ~yp→ p→ (~yz → I || Q ||⌐~p→ P || Z) = ~y → ~yq → q→ ⌐~q → ~yp→ p→(~yz → I || Q ||P || Z) = ~y → ~yq → q→ ⌐~q → ~yp→ p→(~yz → I || Q ||P ||~yz→ z→ Z) = ~y → ~yq → q→ ⌐~q → ~yp→ p→ ~yz →(I || Q ||P || z→ Z) = ~y → ~yq → q→ ⌐~q → ~yp→ p→ ~yz → z→ (I || Q || P || Z) Kết hợp với tính chất lũy đẳng của các chương trình, ta có thể chứng minh được rằng: I || Q || P || Z = ( ~x → ~xq → q→ ⌐~q → ~xp→ p→ ~xz → z □ ~y → ~yq → q→ ⌐~q → ~yp→ p→ ~yz → z)→ (I || Q || P || Z) Khi che giấu các biến thay đổi bên trong ta nhận được: I || Q || P || Z )\{~xq, ~yq, ~xp, ~yp, ~xz, ~yz, ~q} = ( ~x → q→ p → z □ ~y → q→ p → z)→ (I || Q || P || Z) = (~x □ ~y )→ q→ p → z)→ (I || Q || P || Z) Hay I || Q || P || Z = μ(Y):A • ((~x □ ~y )→ q→ p → z)→ Y) (10) -274-
9. Hội nghị Khoa học công nghệ lần thứ XXII Trường Đại học Giao thông vận tải Ta cũng có thể chứng minh kết quả trên bằng ngữ nghĩa quan hệ trong [3] như sau: Mạch trên được mô phỏng bới chương trình S = g(Q||P||Z)*(Q||P||Z) Các trạng thái ổn định (X, Y, Q, P, Z) là: (0, 0, 0, 0, 1) ; (0, 1, 0, 0, 1); (0, 1, 1, 0, 1); (0, 0, 1, 1, 0); (1, 0, 1, 1, 1); (1, 1, 1, 1, 1); (1, 0, 0, 1, 0); (1, 1, 0, 1, 1) Như trong [5] ta đã chứng minh Z, Q, P là 3 chương trình lũy đẳng: • Z lũy đẳng vì không có bộ nhớ (không có quy lui). • Q; Q = {Q |Y’•Q + X} Q = Q • P; P = {P | P•Q + P•Y + Y’•X’•Q} P = P Ta nhận thấy, Z không là đầu vào của P, Q và P không là đầu vào của Q. Do đó theo Định lý 2 và Hệ quả 1 [5], ta có: S = g(Q||P||Z)*(Q||P||Z)) = g((Q||P)||Z)*((Q||P)||Z) = g(Q||P)*(Q||P); g(Z)*Z = g(Q)*Q; g(P)*P; g(Z)*Z = Q; P; Z Như vậy, chương trình có thể biểu diễn dưới dạng kết hợp tuần tự của ba chương trình tuần tự, như đã chỉ ra trong ngữ nghĩa CSP của mạch trong công thức (10). 6. KẾT LUẬN Như vậy bằng việc dùng đại số các tiến trình tuần tự tương tác CSP mô phỏng các mạch tuần tự không đồng bộ, chúng ta đã xác định ngữ nghĩa đại số CSP của các mạch đó và chứng tỏ đây là một các tiếp cận tương đương với việc dùng các chương trình tuần tự với ngữ nghĩa quan hệ [3] để mô tả chúng. Thêm vào đó, việc đưa ra ngữ nghĩa CSP của mạch phần cứng cho phép triển khai các ứng dụng song song dựa trên CSP từ thiết kế, cài đặt phần mềm trên ngôn ngữ lập trình đến chương trình trên ngôn ngữ phần cứng tạo thành quá trình thống nhất trên CSP, đảm bảo tính đúng đắn của nó. TÀI LIỆU THAM KHẢO [1]. C.A.R. Hoare and He Jifeng. Unifying Theory of Programing. Prentice – Hall, (1998). [2]. Tran Van Dung and He Jifeng. A Theory of Combinational Programs, Proceedings, APSEC 2001, Macao, Computer Society Press, pp. 325-329. [3]. Tran Van Dung. On the Stability Semantics of Combinational Programs, Proceedings, ICTAC2005, LNCS 3722, pp. 180-194. [4]. Trần Văn Dũng. Về ngữ nghĩa đại số của chương trình tổ hợp. Tạp chí Tin học và điều khiển, T25, S4 (2009), 1- 13. [5]. Trần Văn Dũng. Đồng hồ cho mạng Petri dựa thành phần. Kỷ hiếu Hội thảo “Các trường đại học kỹ thuật với hoạt động khởi nghiệp và đổi mới sáng tạo của tỉnh Bến tre” (11/2019), 321-328. -275-