Hệ thống kiểu tính cận trên số log cho ngôn ngữ giao dịch đa luồng tối giản

JOURNAL OF SCIENCE OF HNUE DOI: 10.18173/2354-1075.2015-0055 Educational Sci., 2015, Vol. 60, No. 7A, pp. 80-93 This paper is available online at HỆ THỐNG KIỂU TÍNH CẬN TRÊN SỐ LOG CHO NGÔN NGỮ GIAO DỊCH ĐA LUỒNG TỐI GIẢN Trương Anh Hoàng1, Nguyễn Ngọc Khải2 1Trường Đại học Công nghệ - Đại học Quốc Gia Hà Nội 2Trường Đại học Tài nguyên và Môi trường Hà Nội Tóm tắt. Trong bài báo này, chúng tôi đưa ra một hệ thống kiểu để ước lượng cận trên tài nguyên sử dụng của các chương trình đa luồng và sử dụng bộ nhớ giao dịch. Tài nguyên được đơn giản hóa là số vùng bộ nhớ giao dịch được tạo ra. Hệ thống kiểu được xây dựng cho một ngôn ngữ lõi với các lệnh cơ bản nhất liên quan đến việc tạo luồng và giao dịch. Việc sử dụng ngôn ngữ lõi này giúp việc kiểm tra tính đúng đắn và chính xác của việc ước lượng được rõ ràng hơn đồng thời cũng cho phép mở rộng ra các ngôn ngữ sử dụng bộ nhớ giao dịch khác được thuận lợi. Từ khóa: Hệ thống kiểu, biên tài nguyên, bộ nhớ giao dịch, đa luồng, ngôn ngữ lập trình. 1. Mở đầu Bộ nhớ giao dịch phần mềm [12] là một cấu trúc lập trình nhằm thay thế cho cơ chế đồng bộ bộ nhớ dùng chung dựa trên khóa. Một trong những cơ chế giao dịch mạnh cho phép các giao dịch đan xen việc lồng nhau và việc tạo luồng mới trong giao dịch đang mở được mô tả trong [9]. Theo cơ chế này, một giao dịch được gọi là lồng trong giao dịch khác nếu nó bắt đầu và kết thúc trong giao dịch khác; giao dịch đầu gọi là giao dịch cha, giao dịch sau gọi là giao dịch con. Khi lồng nhau, các giao dịch con phải kết thúc (commit) trước giao dịch cha của chúng được kết thúc. Một giao dịch được gọi là đa luồng khi người lập trình có thể tạo ra luồng mới ngay bên trong giao dịch khi nó chưa kết thúc. Các luồng được tạo ra này chạy song song với luồng đang có giao dịch chưa kết thúc. Để cho phép truy cập đồng thời đến các biến dùng chung, luồng mới sẽ tạo bản sao của các biến thuộc các giao dịch đang mở. Khi luồng cha kết thúc một giao dịch, tất cả luồng con của nó đã được tạo ra bên trong giao dịch đó phải cùng kết thúc với luồng cha của chúng. Chúng tôi gọi loại kết thúc này là đồng kết thúc (joint commit) và thời điểm kết thúc này là điểm đồng kết thúc. Các đồng kết thúc này là một dạng đồng bộ ẩn của các luồng chạy song song với nhau. Để cài đặt cơ chế bộ nhớ giao dịch, mỗi giao dịch có một vùng bộ nhớ cục bộ riêng biệt cho từng luồng, được gọi là log, để lưu trữ các biến dùng chung (chia sẻ) để các luồng truy cập độc lập các bản sao của biến dùng chung trong quá trình thực hiện. Mỗi luồng có thể tạo một số giao dịch lồng nhau nên sẽ có tương ứng một số lượng log được tạo ra cho mỗi giao dịch. Hơn nữa, một luồng con khi tạo ra trong một giao dịch cũng sẽ có các bản sao như cha của nó. Khi đồng kết thúc, các log được so sánh với nhau và nếu không có mâu thuẫn trong việc cập nhật các Ngày nhận bài: 6/8/2015. Ngày nhận đăng: 15/11/2015. Liên hệ: Trương Anh Hoàng, e-mail: truonganhhoang@gmail.com 80 Hệ thống kiểu tính cận trên số log cho ngôn ngữ giao dịch đa luồng tối giản biến thì giao dịch được hoàn tất. Ngược lại nếu có mâu thuẫn trong việc cập nhật các biến của các luồng tham gia vào quá trình đồng kết thúc thì giao dịch có thể được thử lại (retry), hoặc hủy bỏ (rollback). Tại các điểm đồng kết thúc, các log được giải phóng, tức là tài nguyên bộ nhớ tương ứng được giải phóng. Cơ chế bộ nhớ giao dịch này tuy có ưu điểm là tạo thuận lợi cho người lập trình nhưng nó cũng gây một số vấn đề không tầm thường như: việc tạo bản sao của các log khi một luồng mới được tạo ra là ngầm, hay việc đồng bộ các trạng thái kết thúc với các trạng thái khác cũng là ngầm. Ngầm ở đây được hiểu là người lập trình không chủ động viết lệnh tạo các log hay lệnh đồng bộ. Các hoạt động ngầm này làm việc ước lượng tài nguyên sử dụng của các chương trình trong các trường hợp này trở nên khó khăn. Hơn nữa, việc tạo bản sao của các log cũng làm ảnh hưởng đến khả năng cùng kết thúc của các luồng đang hoạt động song song, và việc tạo ra nhiều log có thể ảnh hưởng đến sự an toàn của chương trình khi tài nguyên bộ nhớ của các máy đều là hữu hạn. Vì vậy, việc ước lượng cận trên số log cùng tồn tại trong một chương trình bộ nhớ giao dịch đa luồng, lồng nhau có một vai trò quan trọng để đánh giá tính hiệu quả của chương trình. Trong nghiên cứu trước đây [10, 14] chúng tôi đã đưa ra hệ thống kiểu và hiệu ứng để ước lượng cận trên số log cùng tồn tại trong một thời điểm. Tuy nhiên, hệ thống kiểu và hiệu ứng trong nghiên cứu này còn phức tạp và biên tìm được chưa sắc - tức là ước lượng cận trên cao hơn thực tế có thể xảy ra. Trong nghiên cứu này, chúng tôi sẽ đưa ra một hệ thống kiểu mới đơn giản hơn cho một ngôn ngữ cũng được đơn giản hóa nhưng vẫn có đầy đủ các lệnh cơ bản để tạo giao dịch và luồng con, và suy luận biên chính xác hơn. Các đóng góp chính trong bài báo này gồm: • Đưa ra một ngôn ngữ lõi chỉ gồm các lệnh liên quan đến giao dịch và đa luồng. • Trình bày hệ thống kiểu có khả năng xác định cận trên của số log chương trình có thể tạo ra. • Nêu tính chất và chứng minh tính đúng đắn của hệ thống kiểu chúng tôi đề xuất. Ước lượng tài nguyên sử dụng đã được nghiên cứu trong nhiều ngữ cảnh khác nhau. Tuy nhiên, hầu hết các nghiên cứu đều hạn chế trong các ngôn ngữ lập trình tuần tự hoặc hàm. Trong nghiên cứu này, chúng tôi tập trung xác định số lượng log tối đa của các chương trình đa luồng, các cấu trúc đồng bộ phức tạp và ngầm định với các mô hình giao dịch có kế thừa. Hughes và Pareto [8] đã giới thiệu một cấu trúc dữ liệu đệ quy và động để xác định biên tài nguyên sử dụng. Tofte và Talpin [13] sử dụng hệ thống suy luận để mô tả việc quản lí bộ nhớ cho các chương trình thực hiện cấp phát và giải phóng bộ nhớ động. Hofmann và Jost [6] tính toán biên trên không gian heap cho một ngôn ngữ hàm đầu tiên. Wei-Ngan Chin [5] xác minh bộ nhớ sử dụng cho các chương trình hướng đối tượng. Những người lập trình được yêu cầu chú thích về bộ nhớ sử dụng và kích thước liên quan cho các phương thức cũng như việc giải phóng bộ nhớ rõ ràng. Trong [7], Hofmann và Jost sử dụng hệ thống kiểu để tính toán biên không gian heap như một hàm của đầu vào cho một ngôn ngữ hướng đối tượng. Trong [4] các tác giả tính toán cận trên tài nguyên sử dụng của một phương thức sử dụng hàm phi tuyến với các tham số của phương thức. Các biên ở đây chưa được chính xác và nghiên cứu của họ cũng không dựa trên kiểu. Braberman và cộng sự [2] tính toán sấp xỉ hình thức phi tuyến của biên bộ nhớ cho những chương trình Java liên quan đến cả cấu trúc dữ liệu và vòng lặp. Trong [3] các tác giả đề xuất hệ thống kiểu cho các ngôn ngữ thành phần với các thành phần chạy song song nhưng các luồng chạy độc lập. Trong [1], Albert và các cộng sự tính toán kích thước bộ nhớ (heap) của một chương trình là một hàm của biến đầu vào. Trong [11] đề xuất một thuật toán nhanh để xác định tĩnh cận trên của bộ nhớ heap của một lớp chương trình JavaCard. Trong các phân tích của chúng tôi sẽ tập trung vào ngôn ngữ cho phép linh hoạt việc tạo luồng con và linh hoạt trong việc mở, đóng và kéo theo sự đồng bộ ngầm giữa các luồng khi kết thúc giao dịch. Ngôn ngữ và hệ thống kiểu của chúng tôi được tối giản sẽ là nền tảng tốt cho các nghiên cứu sau này về tài nguyên bộ nhớ của các ngôn ngữ sử dụng bộ nhớ giao dịch. 81 Trương Anh Hoàng, Nguyễn Ngọc Khải 2. Nội dung nghiên cứu 2.1. Ví dụ minh họa Để minh họa bài toán và hướng giải quyết chúng tôi sử dụng Đoạn mã 1 dưới đây làm ví dụ minh họa. Trong đoạn chương trình này, cặp lệnh onacid và commit để bắt đầu và kết thúc một giao dịch và chúng phải đi đôi với nhau. Các biểu thức e1, e2, e3 và e4 đại diện cho các đoạn các chương trình con. Lệnh spawn tạo một luồng mới. Đoạn mã 1: Một chương trình lồng nhau và đa luồng. 1 onacid;//thread 0 2 onacid; 3 spawn(e1;commit;commit);//thread 1 4 onacid; 5 spawn(e2;commit;commit;commit);//thread 2 6 commit; 7 e3; 8 commit; 9 e4; 10 commit Hình 1. Các luồng song song, lồng nhau và cùng kết thúc Ngữ nghĩa của chương trình này được minh họa trong Hình 1. Lệnh onacid và lệnh commit được kí hiệu bằng [ và ] tương ứng trong hình. Lệnh spawn tạo ra một luồng mới chạy song song với luồng cha của nó và được mô tả bằng các đường nằm ngang. Luồng mới sẽ tạo bản sao của các log của luồng cha để luồng mới truy cập các biến này một cách độc lập, tránh xung đột với các luồng khác. Trong ví dụ này, khi tạo ra e1 luồng chính đã mở được hai giao dịch, vì vậy luồng 1 thực thi e1 trong hai giao dịch này và phải thực hiện hai lệnh commit để đóng chúng. Các luồng song song của một giao dịch sẽ cùng kết thúc tại một thời điểm được mô tả bằng các hình chữ nhật có đường kẻ chấm chấm. Các cạnh bên phải của hình chữ nhật thể hiện thời điểm đồng bộ này. Giả sử e1 là một giao dịch đơn không có giao dịch con, e2 là một giao dịch với hai giao dịch con lồng nhau (e2=onacid; onacid; commit; commit), e3 là một giao dịch với ba giao dịch con bên trong lồng nhau, và e4 có bốn giao dịch bên trong lồng nhau. Có thể tính tay ra số log tối đa của chương trình là ngay sau khi tạo ra e2. Tại thời điểm đó, e1 đóng góp 3 giao dịch (2 từ luồng chính, và 1 của chính nó), e2 đóng góp 5 giao dịch (3 từ luồng chính, và 2 của chính nó), luồng chính đóng góp 3 giao dịch. Tổng sẽ là 3 + 5 + 3 = 11 giao dịch. Trong thời điểm thực 82 Hệ thống kiểu tính cận trên số log cho ngôn ngữ giao dịch đa luồng tối giản hiện e3 và e4, số giao dịch được mở ít hơn bởi vì nhiều giao dịch đã đóng trước đó. Một điểm khó khăn của việc phân tích đó là phải nắm bắt được những điểm đồng bộ ngầm ở thời điểm biên dịch. Ví dụ trên sử dụng một ngôn ngữ lõi với các lệnh cơ bản nhất liên quan đến việc tạo luồng và giao dịch, và chúng tôi gọi là TM (transactional multi-threaded language). Trong nghiên cứu trước đây của chúng tôi, việc chia tách chương trình thành các thành phần con và sau đó xây dựng các kiểu cho các thành phần con này được thực hiện một cách khá tự do. Điều này dẫn đến một hệ thống kiểu phức tạp vì sau đó chúng ta phải xử lí khá nhiều khả năng kết hợp của các thành phần này. Trong nghiên cứu này, để hạn chế việc kết hợp tùy ý các thành phần, chúng tôi sẽ xác định kiểu cho luồng trong cùng trước, sau đó sẽ kết hợp với các luồng anh chị (cha) của nó, và quá trình này được lặp lại đến khi chỉ còn môt luồng chính. Trong ví dụ này, chúng ta xác định kiểu cho biểu thức trong dòng 5 trước tiên, sau đó kết hợp nó với phần từ dòng 6 tới dòng 10. Tiếp theo dòng 4 sẽ được xác định kiểu với phần từ dòng 5 tới dòng 10. Bây giờ phần từ dòng 4 tới dòng 10 sẽ kết hợp với luồng con trong dòng 3. Sau đó dòng 2 sẽ được xác định kiểu với dòng 3 tới 10, và sau cùng chúng ta có thể xác định kiểu toàn bộ chương trình từ dòng 1 tới dòng 10. Bằng cách này, chúng ta có một ước lượng số log tối đa chính xác hơn. 2.2. Ngôn ngữ TM TM là một ngôn ngữ mệnh lệnh hỗ trợ cấu trúc giao dịch và đa luồng. Đây là những đặc điểm cần thiết của các mô hình tương tranh và các hệ thống giao dịch lồng nhau. P ::= 0 | p(e) |P ‖ P e ::= e1; e2 | e1 + e2 | spawn(e) | onacid | commit Hình 2. Cú pháp của TM 2.2.1. Cú pháp Cú pháp của TM được thể hiện trong Hình 2. Dòng thứ nhất để biểu diễn các luồng/tiến trình. Dòng thứ 2 xác định các lệnh cơ bản tạo thành chương trình. e có thể là e1 nối tiếp bởi e2 hoặc nhận một trong hai giá trị e1 hoặc e2. Dòng sau cùng là ba lệnh để tạo một luồng, bắt đầu và kết thúc một giao dịch. Hai lệnh cuối này chính là các lệnh sử dụng (cấp phát) và giải phóng tài nguyên. 2.2.2. Ngữ nghĩa động Ngữ nghĩa của TM được thể hiện bởi hai tập quy tắc hoạt động: tập quy tắc cho ngữ nghĩa mệnh lệnh (Bảng 1) và tập quy tắc cho ngữ nghĩa giao dịch và đa luồng (Bảng 2). Hiểu một cách tổng quát, môi trường lúc chạy (toàn cục) là một tập hợp các luồng. Mỗi luồng có một môi trường cục bộ là một chuỗi các log. Để quản lí các luồng và log này chúng ta gán cho mỗi luồng và mỗi log một định danh. Phần tiếp theo chúng tôi sẽ định nghĩa một cách hình thức về môi trường cục bộ và môi trường toàn cục. Ngữ nghĩa mệnh lệnh Ngữ nghĩa mệnh lệnh là các quy tắc chuẩn tương tự như các ngôn ngữ thông dụng khác. Ở đây, chúng tôi chỉ trình bày những điểm chính liên quan đến việc tạo và hủy các log của các giao dịch và các luồng. Định nghĩa 2.1 (Môi trường cục bộ). Một môi trường cục bộ E là một dãy hữu hạn các log được gắn nhãn l1:log1; . . . ; lk:logk, trong đó phần tử thứ i của dãy bao gồm một nhãn li (một tên giao 83 Trương Anh Hoàng, Nguyễn Ngọc Khải dịch) và log logi. Cho E = l1:log1; . . . ; lk:logk, ta gọi k là kích cỡ của E, và được kí hiệu là |E|. Kích cỡ |E| là độ sâu của các giao dịch lồng nhau (l1 là giao dịch ngoài cùng, lk là giao dịch trong cùng). Môi trường rỗng/trống kí hiệu là ǫ. E, (e1 + e2); e→ E, (e1; e) L-COND1 E, (e1 + e2); e→ E, (e2; e) L-COND2 Bảng 1. Ngữ nghĩa mệnh lệnh Ngữ nghĩa ở mức cục bộ được biểu diễn dạng E, e → E′, e′. Trong đó E,E′ là các môi trường cục bộ, e, e′ là các biểu thức được đánh giá trong các môi trường đó. Hai quy tắc L-COND1 và L-COND2 được hiểu như việc lựa chọn thực thi một trong hai biểu thức e1 hoặc e2 tùy thuộc vào giá trị các biểu thức điều kiện. Ngữ nghĩa giao dịch và đa luồng Các quy tắc cho các ngữ nghĩa được thể hiện dưới dạng Γ, P ⇒ Γ′, P ′ hoặc Γ, P ⇒ error , trong đó Γ là một môi trường toàn cục và P là một tập tiến trình có dạng p(e). Một môi trường toàn cục bao gồm các môi trường cục bộ của các luồng và được định nghĩa như sau: Định nghĩa 2.2 (Môi trường toàn cục). Một môi trường toàn cục Γ là một ánh xạ xác định từ định danh của luồng tới môi trường cục bộ của nó, Γ = p1:E1, . . . , pk:Ek, trong đó pi là một định danh của luồng và Ei là môi trường cục bộ của luồng pi. E, e→ E′, e′ p : E ∈ Γ ref lect(p,E′,Γ) = Γ′ Γ, P ‖ p(e)⇒ Γ′, P ‖ p(e′) G-PLAIN p′ fresh spawn(p, p′,Γ) = Γ′ Γ, P ‖ p(spawn(e1); e2)⇒ Γ′, P ‖ p(e2) ‖ p′(e1) G-SPAWN l fresh start(l, p,Γ) = Γ′ Γ, P ‖ p(onacid; e)⇒ Γ′, P ‖ p(e) G-TRANS p : E ∈ Γ E = ..; l : log; intranse(Γ, l) = p¯ = p1..pk commit(p¯, E¯,Γ) = Γ′ Γ, P ‖∐k1 pi(commit; ei)⇒ Γ′, P ‖ (∐k1 pi(ei)) G-COMM Γ = Γ′′; p : E |E| = 0 Γ, P ‖ p(commit; e)⇒ error G-ERROR Bảng 2. Ngữ nghĩa giao dịch và luồng Để mô tả ngữ nghĩa của ngôn ngữ, ta cần thêm một số hàm phụ trợ sau: • Hàm ref lect cập nhật thay đổi từ môi trường cục bộ lên môi trường toàn cục: Nếu ref lect(p,E′,Γ) = Γ′ và Γ = p1 : E1, ..., pk : Ek thì Γ′ = p1 : E′1..., pk : E ′ k với|Ei| = |E′i| (với mọi i). • Hàm spawn sinh ra một luồng mới p′ từ luồng cha p: Giả sử Γ = p : E,Γ′′ và p′ /∈ Γ và spawn(p, p′,Γ) = Γ′, thì Γ′ = Γ, p′ : E′ với |E| = |E′|. • Hàm start(l, pi,Γ) tạo ra một giao dịch mới nhãn l từ luồng pi: Nếu start(l, pi,Γ) = Γ′ với Γ = p1 : E1, ..., pi : Ei, ..., pk : Ek và với một lệnh fresh l, thì Γ′ = p1 : E1, ..., pi : E′i, ..., pk : Ek, với |E′i| = |Ei|+ 1. 84 Hệ thống kiểu tính cận trên số log cho ngôn ngữ giao dịch đa luồng tối giản • Hàm intranse(Γ, l) trả lại một tập các luồng trong giao dịch l: Giả sử Γ = Γ′′, p : E với E = E′, l : ρ và intranse(Γ, l) = p¯, thì: - p ∈ p¯ và - với mọi pi ∈ p¯ ta có Γ = ..., pi : (E′i, l : ρi), ... - với mọi luồng p′ với p′ /∈ p¯ và Γ = ..., p′ : (E′, l′ : ρ′), ..., ta có l′ 6= l. • Hàm commit kết thúc một giao dịch: nếu commit(p¯, E¯,Γ) = Γ′ với Γ = Γ′′, p : (E, l : ρ) và p¯ = intranse(Γ, l) thì Γ′ = ..., pj : E′j , ..., pi : E;i , ... trong đó pi ∈ p¯, pj /∈ p¯, pj : Ej ∈ Γ, với |E′j | = |Ej | và |E′i| = |Ei| − 1. Chú ý là các hàm spawn tạo ra nhiều nhãn giống nhau ở các luồng khác nhau và đây là dấu vết để chúng cùng được đồng kết thúc ở quy tắc G-SPAWN. Các quy tắc trong Bảng 2 có nghĩa như sau: • Quy tắc G-PLAIN để cập nhật các thay đổi ở mức cục bộ lên mức toàn cục. Giả sử p : E ∈ Γ, khi luồng p tạo ra biến đổi E, e→ E′, e′ trên môi trường cục bộ E của nó. Hàm ref lect sẽ cập nhật những biến đổi này lên môi trường toàn cục, chuyển từ môi trường Γ thành Γ′. • Quy tắc G-SPAWN dùng cho trường hợp tạo luồng mới với lệnh spawn. Lệnh spawn(e1) tạo ra luồng mới p′ thực thi e1 song song với luồng cha p, biến đổi môi trường từ Γ sang Γ′. • Quy tắc G-TRANS dùng trong trường hợp luồng p tạo một giao dịch mới với lệnh onacid. Giao dịch mới với nhãn l được sinh ra, môi trường được biến đổi từ Γ sang Γ′. • Quy tắc G-COMM để thực hiện việc kết thúc các giao dịch. Giao dịch hiện tại của luồng p là l. Tất cả các luồng trong giao dịch l phải cùng kết thúc (commit) khi giao dịch l kết thúc. • Quy tắc G-ERROR dùng trong trường hợp việc kết thúc một giao dịch không thành công. Trong trường hợp luồng p thực hiện việc kết thúc giao dịch bên ngoài môi trường của nó nghĩa là |E| = 0 thì sẽ trả lại kết quả lỗi (error). 2.3. Hệ thống kiểu Mục đích của hệ thống kiểu của chúng ta là để xác định số log tối đa có thể được tạo ra của một chương trình TM. Ở đây chúng tôi đề xuất kiểu của một đoạn chương trình là một dãy số có dấu. Các dãy số có dấu này là trừu tượng của các hành vi giao dịch của đoạn chương trình. 2.3.1. Kiểu Để mổ tả hành vi giao dịch của một đoạn chương trình, chúng tôi sử dụng một tập bốn kí hiệu {+,−,¬, ♯}. Kí hiệu + và − lần lượt mô tả cho sự bắt đầu và kết thúc một giao dịch. Kí hiệu ¬ miêu tả các điểm đồng kết thúc của các giao dịch trong các luồng song song và ♯ miêu tả số log tối đa được tạo ra. Để tiện lợi hơn cho việc tính toán về sau trên các dãy này, chúng ta gán một kí hiệu với một số tự nhiên không âm n ∈ N+ = {0, 1, 2, ..} thành dạng số có dấu. Vì vậy, các kiểu này sử dụng dãy hữu hạn của tập số có dấu TN = {+n , −n , ♯n , ¬n | n ∈ N+}. Chúng tôi sẽ cố gắng để đưa ra các quy tắc để miêu tả một thành phần (biểu thức) của TM bằng một dãy số có dấu. Một đoạn chương trình có kiểu, +n (−n ) được hiểu là có liên tiếp n onacid (commit) và với ¬n thì được hiểu là trong thành phần này có n luồng cần phải đồng bộ với một onacid nào đó để hoàn tất một giao dịch, và với kí hiệu ♯n thì được hiểu là thành phần này tạo ra tối đa n log. Trong quá trình tính toán, phần tử có giá trị 0 có thể xuất hiện nhưng nó không ảnh hưởng đến ngữ nghĩa của chuỗi nên chúng ta sẽ tự động bỏ chúng. Để đơn giản khi trình bày, chúng ta cũng được chèn phần tử ♯0 khi cần thiết. Chúng ta dùng s cho các phần tử thuộc TN, kí hiệu T N¯ là tập hợp của tất cả các chuỗi của các số có dấu, dùng S cho các phần tử thuộc T N¯ và m,n, l, .. thuộc N. Các chuỗi rỗng được kí hiệu là ǫ. Đối với một chuỗi S chúng ta kí hiệu độ dài là |S|, và kí hiệu S(i) cho phần tử thứ i của 85 Trương Anh Hoàng, Nguyễn Ngọc Khải S. Đối với một số có dấu s, chúng ta kí hiệu tag(s) là tag của s, và |s| là số tự nhiên tương ứng của s (ví dụ s = tag(s)|s|). Đối với một chuỗi S ∈ T N¯, chúng ta kí hiệu tag(S) cho chuỗi của các tag của các phần tử của S, ví dụ, tag(s1 . . . sk) = tag(s1) . . . tag(sk) và kí hiệu {S} cho tập các kí hiệu xuất hiện trong S. Để đơn giản chúng ta cũng kí hiệu tag(s) ∈ S thay cho tag(s) ∈ {S}. Tập T N¯ có thể được phân chia thành các lớp tương đương. Các phần tử trong cùng lớp tương đương sẽ cùng biểu diễn một hành vi giao dịch. Trong mỗi lớp này chúng ta sẽ sử dụng chuỗi rút gọn nhất để đại diện cho lớp đó và gọi nó là chuỗi chính tắc. Định nghĩa 2.3 (Chuỗi chính tắc). Một chuỗi S là chuỗi chính tắc nếu tag(S) không chứa chuỗi con ‘−−’, ‘♯♯’, ‘++’, ‘+−’, ‘+♯−’, ‘+¬’ hoặc ‘+♯¬’ và |S(i)| > 0 với mọi i. Ở đây chúng ta thường có thể đơn giản/rút gọn chuỗi S mà không làm thay ngữ nghĩa của nó. Hàm seq dưới đây sẽ rút gọn một chuỗi S thành một chuỗi chính tắc. Trong định nghĩa này mẫu +− không xuất hiện bên trái, nhưng chúng ta có thể chèn ♯0 để áp dụng. Hai mẫu ‘+¬’ và ‘+♯¬’ sẽ được xử lí bởi hàm jc ở phần sau. Định nghĩa 2.4 (Đơn giản hóa). Hàm seq được định nghĩa đệ quy như sau: seq(S) = S khi S là chính tắc seq(S ♯m ♯nS′) = seq(S ♯max(m,n)S′) seq(S +m +nS′) = seq(S +(m+ n)S′) seq(S −m −nS′) = seq(S −(m+ n)S′) seq(S +m ♯l −nS′) = seq(S +(m− 1) ♯(l + 1) −(n− 1)S′) Như minh họa trong Hình 1, các luồng được đồng bộ bằng các đồng kết thúc (hình chữ nhật