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

Bài viết 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 để 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ộ.
Nội dung trích xuất từ tài liệu:
Ngữ nghĩa CSP cho các mạch tuần tự không đồng bộ 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- 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- 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ì ...