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

Chia sẻ: ViHasaki2711 ViHasaki2711 | Ngày: | Loại File: PDF | Số trang:14

Thêm vào BST

Báo xấu

25
lượt xem 3
download

Download Vui lòng tải xuống để xem tài liệu đầy đủ

Bài viết đư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.

Chủ đề:

Bình luận(0) Đăng nhập để gửi bình luận!

Lưu

Nội dung Text: 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 http://stdb.hnue.edu.vn 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 1 Trường Đại học Công nghệ - Đại học Quốc Gia Hà Nội 2 Trườ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 k 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 ′ , Γ) = Γ′ G-PLAIN Γ, P k p(e) ⇒ Γ′ , P k p(e′ ) p′ f resh spawn(p, p′ , Γ) = Γ′ G-SPAWN Γ, P k p(spawn(e1 ); e2 ) ⇒ Γ′ , P k p(e2 ) k p′ (e1 ) l f resh start(l, p, Γ) = Γ′ G-TRANS Γ, P k p(onacid; e) ⇒ Γ′ , P k p(e) p : E ∈ Γ E = ..; l : log; intranse(Γ, l) = p¯ = p1 ..pk commit(¯ ¯ Γ) = Γ′ p, E, G-COMM Γ, P k k1 pi (commit; ei ) ⇒ Γ′ , P k ( k1 pi (ei )) ` ` Γ = Γ′′ ; p : E |E| = 0 G-ERROR Γ, P k p(commit; e) ⇒ 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 : E1′ ..., pk : Ek′ với |Ei | = |Ei′ | (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 f resh l, thì Γ′ = p1 : E1 , ..., pi : Ei′ , ..., pk : Ek , với |Ei′ | = |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 : (Ei′ , 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(¯ ¯ Γ) = Γ′ với Γ = Γ′′ , p : (E, l : ρ) p, E, ′ ′ và p¯ = intranse(Γ, l) thì Γ = ..., pj : Ej , ..., pi : E;i , ... trong đó pi ∈ p¯, pj ∈ / p¯, pj : Ej ∈ Γ, với |Ej′ | = |Ej | và |Ei′ | = |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 T N = { +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 T N, 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 ¯ chúng ta kí hiệu tag(S) cho chuỗi của các của s (ví dụ s = tag(s) |s|). Đối với một chuỗi S ∈ T N, 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}. ¯ 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 Tập T N đươ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 ♯n S ′ ) = seq(S ♯max(m, n) S ′ ) seq(S +m +n S ′ ) = seq(S +(m + n) S ′ ) seq(S −m −n S ′ ) = seq(S −(m + n) S ′ ) seq(S +m ♯l −n S ′ ) = 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 nét đứt). Vì vậy các đồng kết thúc này tách một luồng thành các đoạn và chỉ một số đoạn có thể chạy song song với nhau. Trong ví dụ trên e1 có thể chạy song song với e2 và e3, nhưng không chạy song song được với e4. Với kiểu của chúng tôi đưa ra cho biểu thức e, các đoạn có thể được xác định bằng việc xem xét kiểu của biểu thức e bên trong spawn(e) xem có các thành phần − hoặc ¬ không. Ví dụ, trong spawn(e1 ); e2 , nếu chuỗi chính tắc của e1 có − hoặc ¬, thì một số đoạn của e1 phải đồng bộ với đoạn của e2 . Hàm merge trong Định nghĩa 2.6 được sử dụng trong tình huống này, nhưng để định nghĩa nó chúng ta cần một vài hàm phụ. Với S ∈ T N ¯ và sig ∈ {+, −, ¬, ♯}, chúng ta định nghĩa hàm phụ f irst(S, sig) trả về chỉ số i nhỏ nhất có dấu là sig, tức là tag(S(i)) = sig. Nếu không có phần tử như vậy, hàm sẽ trả về 0. Một lệnh kết thúc giao dịch có thể là một kết thúc thường (cục bộ) hoặc một đồng kết thúc. Ban đầu, chúng ta giả sử tất cả các lệnh kết thúc đều là kết thúc thường. Sau đó nếu chúng ta thấy không có lệnh bắt đầu giao dịch (onacid) để khớp với lệnh kết thúc cục bộ thì chúng ta đổi kết thúc này thành một đồng kết thúc. Hàm sau đây thực hiện công việc đó và nó chuyển một chuỗi chính tắc (không có phần tử +) thành một chuỗi đồng bộ. Định nghĩa 2.5 (Chuyển dạng). S = s1 . . . sk là một chuỗi chính tắc, giả sử i = f irst(S, −). Hàm join(S) sẽ thay thế − trong S bằng ¬ như sau: join(S) = S nếu i = 0 ¬ join(S) = s1 ..si−1 1 join( −(|si | − 1) si+1 ..sk ) nếu i 6= 0 Bởi vì hàm join là lũy đẳng, định nghĩa này là hợp lệ. Chú ý là ở đây dạng chính tắc S chỉ chứa các phần tử ♯ xen kẽ với các phần tử − hoặc ¬. Chuỗi đồng bộ được sử dụng cho các biểu 86 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 thức trong spawn hoặc một phần của luồng chính. Các chuỗi đồng bộ này được hợp với nhau theo định nghĩa sau. Định nghĩa 2.6 (Hợp). S1 và S2 là các chuỗi đồng bộ với số lượng các phần tử ¬ trong S1 và S2 là như nhau. Hàm merge được định nghĩa đệ quy như sau: merge( ♯m1 , ♯m2 ) = ♯(m1 + m2 ) merge( ♯m1 ¬ n1 S1′ , ♯m2 ¬ n2 S2′ ) = ♯(m1 + m2 ) ¬ (n1 + n2 ) merge(S1′ , S2′ ) Định nghĩa là hợp lệ vì S1 , S2 là các chuỗi đồng bộ nên chúng chỉ có các phần tử ♯ và ¬. Hơn nữa, số lượng 6= là như nhau trong giả thiết của định nghĩa. Vì vậy, chúng ta có thể chèn ♯0 để tạo ra hai chuỗi phù hợp với định nghĩa. Đối với các lệnh điều kiện e1 + e2 , chúng ta cần hành vi giao dịch của chúng với bên ngoài phải tương tự nhau. Tức là, khi loại bỏ tất cả các phần tử ♯ của chúng thì hai chuỗi còn lại phải giống hệt nhau. Giả sử S1 và S2 là hai chuỗi như vậy thì chúng ta có thể có Si = ♯mi ∗ n Si′ , i = 1, 2, ∗ = {+, −, ¬}, trong đó S1′ và S2′ có các giao dịch tương tự. Với S1 và S2 này, chúng ta định nghĩa phép toán chọn như sau: Định nghĩa 2.7 (Chọn). S1 và S2 là hai chuỗi mà nếu loại bỏ tất cả các phần tử ♯ của chúng thì hai chuỗi là giống hệt nhau. Hàm alt được định nghĩa đệ quy như sau: alt( ♯m1 , ♯m2 ) = ♯max(m1 , m2 ) alt( ♯m1 ∗ n S1′ , ♯m2 ∗ n S2′ ) = ♯max(m1 , m2 ) ∗ n alt(S1′ , S2′ ) 2.3.2. Các quy tắc kiểu T-ONACID T-COMMIT −1 ⊢ onacid : +1 1 ⊢ commit : −1 n⊢e:S n 1 ⊢ e 1 : S1 n2 ⊢ e2 : S2 S = seq(S1 S2 ) T-SPAWN T-SEQ n ⊢ spawn(e) : join(S)ρ n1 + n2 ⊢ e 1 ; e 2 : S n1 ⊢ e1 : S1 n2 ⊢ e2 : S2ρ S = jc(S1 , S2 ) T-JC n1 + n2 ⊢ e 1 ; e 2 : S n ⊢ e1 : S1ρ n ⊢ e2 : S2ρ S = merge(S1 , S2 ) T-MERGE n ⊢ e1 ; e2 : S ρ kind(Ti ) n⊢e:S n ⊢ ei : T i i = 1, 2 kind(T1 ) = kind(T2 ) Ti = Si T-PREP T-COND n ⊢ e : join(S)ρ n ⊢ e1 + e2 : alt(S1 , S2 )kind(S1 ) Bảng 3. Quy tắc kiểu Cú pháp ngôn ngữ kiểu T được định nghĩa như sau: T = S | Sρ S ρ được sử dụng cho biểu thức spawn để đánh dấu chúng cần được đồng bộ với luồng cha của chúng. Chúng ta định nghĩa hàm kind(T ) trả về trống cho kiểu thông thường S hoặc ρ nếu T có dạng S ρ . 87 Trương Anh Hoàng, Nguyễn Ngọc Khải Môi trường kiểu cung cấp thông tin ngữ cảnh cho biểu thức đang được tính kiểu. Các phát biểu về kiểu có dạng sau: n⊢e:T Trong đó n ∈ N là môi trường kiểu. Khi n là dương thì nó thể hiện số giao dịch đang mở mà e sẽ đóng bởi kết thúc thường hoặc đồng kết thúc trong e. Các quy tắc kiểu cho các phép tính của chúng tôi được mô tả trong Bảng 3. Ở đây chúng ta ngầm hiểu là qui tắc được áp dụng khi các hàm tương ứng seq, jc, merge, alt là có thể thực hiện được. Tức là các đối số của chúng đáp ứng các điều kiện của hàm. Quy tắc T-SPAWN chuyển đổi S thành chuỗi đồng bộ và tạo ra kiểu mới bởi ρ để có thể hợp các luồng chạy song song với nó bằng qui tắc T-MERGE. Quy tắc T-PREP cho phép chúng ta tạo một kiểu phù hợp cho e2 để áp dụng T-MERGE. Các quy tắc còn lại thì khá tự nhiên theo ngữ nghĩa của chương trình, ngoại trừ quy tắc T-JC có hàm jc. Hàm này sẽ được giải thích trước khi chúng ta định nghĩa hình thức nó ở Định nghĩa 2.8. Trong quy tắc T-JC, e2 có thể có một vài đoạn, và l (trong Định nghĩa 2.8) là số các luồng cùng kết thúc. Phần tử + cuối cùng trong S1 , là +n , sẽ được khớp với phần tử ¬ đầu tiên trong S2 , là ¬ l . Nhưng sau +n , có thể có một phần tử ♯, gọi là ♯n′ , và số lượng log cục bộ tối đa cho +n ♯n′ là n + n′ (nhưng chúng ta sẽ định nghĩa từng bước một vì vậy trong định nghĩa sau đây của jc chúng ta chỉ thêm 1 vào n′ tại một thời điểm). Tương tự, trước ¬ l có thể có một ♯l′ , vì vậy số lượng log tối đa ở điểm này là ít nhất l + l′ . Sau khi gỡ bỏ một + từ S1 và một ¬ từ S2 chúng ta rút gọn chuỗi mới để có thể áp dụng đệ quy tiếp jc. Do đó chúng ta có định nghĩa hình thức cho jc như sau. Định nghĩa 2.8 (Đồng kết thúc). Hàm jc được định nghĩa đệ quy như sau: jc(S1′ +n ♯n′ , ♯l′ ¬ l S2′ ) = jc(seq(S1′ +(n − 1) ♯(n′ + 1) ), seq( ♯(l′ + l) S2′ )) if l > 0 jc( ♯n′ , ♯l′ ¬ l S2′ ) = seq( ♯max(n′ , l′ ) ¬ l S2′ ) otherwise Vì kiểu của chúng ta thể hiện các hành vi của một đoạn chương trình nên một chương trình có kiểu hợp lệ sẽ có kiểu là một phần tử đơn ♯n và n là số log tối đa cùng tồn tại khi chương trình chạy. Định nghĩa 2.9 (Kiểu hợp lệ). Một biểu thức e có kiểu hợp lệ nếu tồn tại một kiểu dẫn xuất cho e sao cho 0 ⊢ e : ♯n với n nào đó. Một phát biểu kiểu có một đặc điểm đó là môi trường của nó chỉ đủ để các giao dịch đang mở (đồng) kết thúc trong e như mô tả bởi T . Định lý 2.1 (Tính chất của một phát biểu kiểu). Nếu n ⊢ e : T và n ≥ 0 thì sim( +n , T ) = ♯m và m ≥ n trong đó sim(T1 , T2 ) = seq(jc(S1 , S2 )) với Si là Ti được bỏ ρ. Chứng minh. Bằng phương pháp quy nạp dựa trên các quy tắc xác định kiểu được mô tả trong Bảng 3. • Trường hợp T-ONACID không áp dụng bởi vì n < 0. • Trường hợp T-COMMIT là tầm thường vì sejc( +1 −1 ) = ♯1 vì m = 1 = n. • Đối với T-SEQ, theo giả thuyết quy nạp (IH) chúng ta có seq(jc( +ni , Si )) = seq( +ni Si ) = ♯m với i = 1, 2 bởi vì S không có các phần tử ¬. Cần phải chứng minh rằng i i 88 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 sim( +(n1 + n2 ) , S) = ♯m và m ≥ m1 + m2 . Ta có: sim( +(n1 + n2 ) , S) = seq(jc( +(n1 + n2 ) , seq(S1 S2 ))) = seq( +n2 +n1 S1 S2 ) ¬∈ / S1 S2 = seq( +n2 ( +n1 S1 )S2 ) Định nghĩa 2.4 + ♯ = seq( n2 m1 S2 )) IH = ♯(m1 + m2 ) IH, Định nghĩa 2.4 • For T-JC, theo giả thuyết quy nạp ta có seq( +n1 S1 ) = ♯m1 and seq(jc( +n2 , S2 )) = ♯m2 . Tương tự như trường hợp trước, ta có: sim( +(n1 + n2 )) , S) = seq(jc( +(n1 + n2 )) , jc(S1 , S2 ))) S = jc(S1 , S2 ) = seq(jc( +(n1 + n2 ) S1 , S2 ))) jc = seq(jc( +n2 ♯m1 , S2 ))) IH ♯ = max(n2 + m1 , m2 ) jc, IH ≥ ♯max(n2 + n1 ) m1 ≥ n1 theo IH • Đối với T-MERGE, theo giả thuyết quy nạp, ta có: seq(jc( +n1 , S1 ) = ♯m 1 và seq(jc( +n2 S2 ) = ♯m2 . Tương tự như trường hợp trước, ta có: seq(jc( +n , S)) = seq(jc( +n , merge(S1 , S2 ))) S = merge(S1 , S2 ) + + = seq(jc( n , S1 )) + seq(jc( n , S2 )) tính chất của S1 , S2 ♯ = (m1 + m2 ) IH • Đối với các quy tắc còn lại, bổ đề đúng theo các giả thuyết quy nạp. Xác định kiểu cho chương trình ví dụ Bây giờ ta sẽ thử tạo một kiểu dẫn xuất cho chương trình trong Đoạn mã 1. Kí hiệu elm cho phần của chương trình từ dòng l tới dòng m. Đầu tiên, sử dụng T-SEQ, T-ONACID, T-COMMIT ta có các biểu thức bên trong spawn ở dòng 5 có kiểu là ♯2 −1 −1 −1 . Sau đó, áp dụng quy tắc T-SPAWN, ta có: 3 ⊢ e55 : ( ♯2 ¬ 1 ¬ 1 ¬ 1 )ρ Bây giờ, ta có thể sử dụng T-MERGE và cần một biểu thức như vậy mà kiểu của nó phù hợp với ♯2 ¬ 1 ¬ 1 ¬ 1 . Ta tìm được e6 thỏa mãn điều kiện này bởi vì kiểu của nó được suy diễn sử dụng 10 các quy tắc T-SEQ, T-ONACID, T-COMMIT như: 3 ⊢ e610 : −1 ♯3 −1 ♯4 −1 Bằng cách áp dụng T-PREP, ta có một kiểu phù hợp với (2.3.2.). Vì vậy, ta có thể áp dụng với T-MERGE và có: 3 ⊢ e510 : ( ♯2 ¬ 2 ♯3 ¬ 2 ♯4 ¬ 2 )ρ Bây giờ có thể áp dụng T-JC để có kiểu cho e410 : 2 ⊢ e410 : ♯4 ¬ 2 ♯4 ¬ 2 vì jc( +1 , ♯2 ¬ 2 ♯3 ¬ 2 ♯4 ¬ 2 ) = seq( ♯4 ♯3 ¬ 2 ♯4 ¬ 2 ) = ♯4 ¬ 2 ♯4 ¬ 2 . Bằng cách tương tự, ta có thể tính kiểu cho e310 : 2 ⊢ e310 : ♯5 ¬ 3 ♯4 ¬ 3 89 Trương Anh Hoàng, Nguyễn Ngọc Khải Áp dụng T-JC với −1 ⊢ e12 : ♯2 ta có: 0 ⊢ e110 : ♯11 Chương trình có kiểu phù hợp và số lượng log tối đa cùng tồn tại trong suốt quá trình chương trình chạy là 11. Tính chính xác hơn của hệ thống kiểu Hệ thống kiểu của chúng tôi sắc hơn hệ thống kiểu trong các nghiên cứu trước đây [14] qua ví dụ chương trình onacid; onacid; commit; spawn(commit); commit;. Biểu thức trong dòng 4-5 có kiểu ( ¬ 2 )ρ . Dòng 1-3 có kiểu +1 ♯1 . Áp dụng quy tắc T-JC ta có jc( +1 ♯1 , ¬ 2 ) = ♯max(1 + 1, 0 + 2) = ♯2 . Hệ thống kiểu trước đây của chúng tôi sẽ trả lại biên là ♯3 , chúng không chính xác bằng biên ♯2 khi tính bằng hệ thống kiểu trong bài báo này. Đoạn mã 2: Chương trình ví dụ chứng minh tính sắc của biên. 1 onacid; 2 onacid; 3 commit; 4 spawn(commit); 5 commit 2.4. Tính đúng đắn Để chứng minh tính đúng của hệ thống kiểu, ta cần chứng minh một chương trình có kiểu hợp lệ không có số log (tại bất kì thời điểm nào trong quá trình thực hiện của chương trình) lớn hơn số thể hiện trong kiểu của nó. Ta gọi chương trình có kiểu hợp lệ là e và kiểu của nó là ♯n . Ta cần chứng minh khi thực thi e theo ngữ nghĩa trong Phần 2.2., số log trong môi trường toàn cục luôn nhỏ hơn n. Một trạng thái của chương trình là một cặp Γ, P trong đó Γ = p1 : E1 ; . . . ; pk : Ek và P = k1 pi (ei ). Ta nói rằng Γ thỏa mãn P , kí hiệu là Γ |= P , nếu tồn tại S1 , . . . , Sk mà ` |Ei | ⊢ ei : Si với mọi i = 1, . . . , k. Với mỗi i, Ei miêu tả số log đã được tạo ra hoặc sao chép trong luồng pi và Si miêu tả số log sẽ được tạo ra khi thực thi ei . Vì vậy, luồng pi có hành vi về log được miêu tả bởi sim( +|Ei | , Si ), trong đó hàm sim được định nghĩa trong Định lí 2.1. Ta sẽ chứng minh rằng sim( +|Ei | , S) = ♯n với một số n. Ta kí hiệu giá trị n này là |Ei , Si |. Tổng số log của một trạng thái chương trình, bao gồm trong Γ và các log sẽ được tạo ra khi thực thi phần còn lại của chương trình, được kí hiệu là |Γ, P |, được định nghĩa như sau: k X |Γ, P | = |Ei , Si | i=1 Bởi vì |Γ, P | thể hiện số log tối đa từ trạng thái hiện tại và |Γ| là số log ở trạng thái hiện tại, chúng ta có bổ đề sau. Bổ đề 2.1 (Trạng thái). Nếu Γ |= P thì |Γ, P | ≥ |Γ|. Chứng minh. Theo định nghĩa của |Γ, P | và |Γ|, ta chỉ cần chứng minh |Ei , Si | ≥ |Ei | với mọi i. Điều này đúng theo Định lí 2.1. Bổ đề 2.2 (Bất biến cục bộ). Nếu E, e → E ′ , e′ , và |E| ⊢ e : S thì tồn tại S ′ sao cho |E ′ | ⊢ e′ : S ′ và |E, S| ≥ |E ′ , S ′ |. 90 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 Chứng minh. Việc chứng minh được thực hiện bằng cách kiểm tra trực tiếp các luật ngữ nghĩa đối tượng trong Bảng 1. Bổ đề 2.3 (Bất biến toàn cục). Nếu Γ |= P và Γ, P ⇒ Γ′ , P ′ thì Γ′ |= P ′ và |Γ, P | ≥ |Γ′ , P ′ |. Chứng minh. Việc chứng minh được thực hiện bằng cách kiểm tra từng quy tắc một tất cả các quy tắc ngữ nghĩa trong Bảng 2. Với mỗi quy tắc, ta cần chứng minh hai phần: (i) Γ′ |= P ′ và (ii) |Γ, P | ≥ |Γ′ , P ′ |. • Với quy tắc G-SPAWN, từ giả thiết Γ |= P và định nghĩa của |= ta có |E| ⊢ spawn(e1 ); e2 : S và |E, S| = n với một số E, S, n. Với G-SPAWN, ta cần chứng minh hai phần tử mới trong Γ′ là |E| ⊢ spawn(e1 ) : S1 và |E| ⊢ e2 : S2 cho S1 , S2 , điều này được suy ra trực tiếp từ T-MERGE vì spawn(e1 ) chỉ có thể kết hợp với e2 trong quy tắc kiểu này. Thêm nữa, ta có S = merge(S1 , S2 ). Theo định nghĩa của merge, ta có số ¬ trong S, S1 và S2 là tương tự, và theo định nghĩa của jc, nó bằng |E|. Vì vậy |E, Si | = ni với một số ni với i = 1, 2. Vì vậy (i) được chứng minh. Đối với (ii), trước tiên, theo định nghĩa của merge và jc ta có n = n1 +n2 . Ta cần chứng minh |Γ, P |−|Γ′ , P ′ | ≥ 0. Bởi vì Γ và Γ′ chỉ khác trong luồng E, E1 , E2, ta có |Γ, P |−|Γ′ , P ′ | = |E, S| − |E, S1 | − |E, S2 | = n − n1 − n2 = 0. Vì vậy (ii) được chứng minh. • Đối với G-TRANS, tương tự như các trường hợp trước, theo giả thiết ta có |E| ⊢ onacid; e : S và |e, S| = n đối với một số E, S, n. Quy tắc G-TRANS tạo ra một log mới trong E vì vậy ta cần chứng minh |E| + 1 ⊢ e : S ′ cho một số S ′ . Bởi vì onacid; e có thể được định kiểu bởi T-SEQ hoặc T-JC, ta có hai trường hợp cần xem xét. - Với quy tắc T-SEQ, (i) được suy ra trực tiếp bởi quy tắc kiểu khi thành phần đầu tiên là −1 ⊢ onacid : +1. Đối với (ii), tương tự như các trường hợp trước, ta có |Γ, P | − |Γ′ , P ′ | = | +|E| , +1 S ′ | − | +(|E| + 1) , S ′ | = 0. Vì vậy (ii) được chứng minh. - Với quy tắc T-JC, (i) được suy ra trực tiếp bởi quy tắc kiểu khi thành phần đầu tiên là −1 ⊢ onacid : +1 . Đối với (ii) ta có |Γ, P | − |Γ′ , P ′ | = | +|E| , jc( +1 , S ′ )| − | +(|E| + 1) , S ′ | = sim(|E|, jc( +1 , S ′ ) − sim( +(|E| + 1) , S ′ ) = seq(jc(|E|, jc( +1 , S ′ )) − seq(jc( +(|E| + 1) , S ′ )) = seq(jc(|E|, jc( +1 , S ′ )) − seq(jc( +|E| , jc( +1 , S ′ ))) =0 Vì vậy (ii) được chứng minh. • Đối với quy tắc G-COMM, với giả thuyết Γ |= P ta có Ei ⊢ commit; ei : Si đối với một số Ei , Si , i = 1..k′ . Vì commit; ei có thể được xác định kiểu bởi T-SEQ và commit là một joint commit, (i) được suy ra bởi quy tắc kiểu khi biểu thức đầu tiên là +1 ⊢ commit : −1 và ta có Si = ¬ 1 Si′ trong đó Si′ là kiểu của ei . Đối với (ii) ta có: |Γ, P | − |Γ′ , P ′ | Pk′ = 1 (|Ei , ¬ 1 Si′ | − |Ei′ , Si′ |) Pk′ = 1 (seq(jc( +|Ei | , ¬ 1 Si′ )) − seq(jc( +|Ei′ | , Si′ ))2cm định nghĩa |E, S| 91 Trương Anh Hoàng, Nguyễn Ngọc Khải k ′ X = (seq(jc( +|Ei | , ¬ 1 Si′ )) − seq(jc( +(|Ei | − 1) , Si′ )) |Ei′ | = |Ei | − 1 1 k′ X = (seq(jc( +(|Ei | − 1) , ♯1 Si′ )) − seq(jc( +(|Ei | − 1) , Si′ )) định nghĩa jc 1 ≥0 Vì vậy (ii) được chứng minh. • Các quy tắc còn lại được chứng minh tương tự. Tiếp theo chúng ta xem xét tính đúng đắn của hệ thống kiểu đã đề xuất. Định lý 2.2 (Tính đúng đắn). Giả sử 0 ⊢ e : ♯n và p1 : ǫ, p1 (e) ⇒∗ Γ, P . Thì |Γ| < n. Chứng minh. Với môi trường ban đầu ta có |p1 : ǫ, p1 (e)| = sim(0, ♯n ) = ♯n . Vì vậy từ Bổ đề 2.2, 2.3 và Định lí 2.1, định lí được chứng minh bằng quy nạp theo độ dài của dẫn xuất. Định lí cuối cùng này đã khẳng định nếu chương trình có kiểu hợp lệ, thì chương trình đó khi thực hiện sẽ không bao giờ tạo ra số log cùng tồn tại lớn hơn giá trị thể hiện trong kiểu của chương trình. 3. Kết luận Chúng tôi đã trình bày một hệ thống kiểu cho một ngôn ngữ lập trình lập trình được tối giản, chỉ có các lệnh liên quan đến bộ nhớ giao dịch và tạo luồng. Hệ thống kiểu này có một số ưu điểm so với hệ thống kiểu trước đây [10, 14] ở điểm vừa đơn giản hơn lại vừa tính được chính xác hơn số lượng log tối đa cùng tồn tại trong quá trình thực thi của chương trình. Hệ thống kiểu cho ngôn ngữ lõi này là nền tảng để áp dụng vào các ngôn ngữ lập trình trên thực tế. Đây cũng là hướng nghiên cứu tiếp theo của chúng tôi để áp dụng cho các ngôn ngữ lập trình trên thực tế. Lời cảm ơn. Nghiên cứu này được tài trợ bởi Quỹ Phát triển khoa học và công nghệ Quốc gia (NAFOSTED) trong đề tài mã số 102.03-2014.23. TÀI LIỆU THAM KHẢO [1] Elvira Albert, Samir Genaim, and Miguel Gomez-Zamalloa, 2007. Heap space analysis for Java bytecode. In ISMM ’07, New York, NY, USA. ACM. [2] David Aspinall, Robert Atkey, Kenneth MacKenzie, and Donald Sannella, 2010. Symbolic and analytic techniques for resource analysis of Java bytecode. In TGC’10, number 6084 in LNCS. Springer-Verlag. [3] Marc Bezem, Dag Hovland, and Hoang Truong, 2012. A type system for counting instances of software components. Theor. Comput. Sci., 458:29-48. [4] Victor Braberman, Diego Garbervetsky, and Sergio Yovine, 2006. A static analysis for synthesizing parametric specifications of dynamic memory consumption. Journal of Object Technology, 5(5). [5] Wei-Ngan Chin, Huu Hai Nguyen, Shengchao Qin, and Martin C. Rinard, 2005. Memory usage verification for OO programs. In Proceedings of SAS ’05, Volume 3672 of LNCS. Springer-Verlag. 92 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 [6] Martin Hofmann and Steffen Jost, 2003. Static prediction of heap space usage for first-order functional programs. In Proceedings of POPL ’03. ACM. [7] Martin Hofmann and Steffen Jost, 2006. Type-based amortised heap-space analysis (for an object-oriented language). In Peter Sestoft, editor, Proceedings of ESOP 2006, volume 3924 of LNCS. Springer-Verlag. [8] John Hughes and Lars Pareto, 1999. Recursion and dynamic data-structures in bounded space: Towards embedded ML programming. SIGPLAN Notices, 34(9). [9] Suresh Jagannathan, Jan Vitek, Adam Welc, and Antony Hosking, 2005. A transactional object calculus. Sci. Comput. Program., 57(2):164-186. [10] Thi Mai Thuong Tran, Martin Steffen, and Hoang Truong, 2013. Compositional static analysis for implicit join synchronization in a transactional setting. In Software Engineering and Formal Methods, Volume 8137 of LNCS, pages 212-228. Springer Berlin Heidelberg. [11] Tuan-Hung Pham, Anh-Hoang Truong, Ninh-Thuan Truong, and Wei-Ngan Chin, 2008. A fast algorithm to compute heap memory bounds of Java Card applets. In SEFM’08. [12] Nir Shavit and Dan Touitou, 1995. Software transactional memory. In Symposium on Principles of Distributed Computing, pages 204 - 213. [13] Mads Tofte and Jean-Pierre Talpin, 1997. Region-based memory management. Information and Computation, 132(2). [14] Xuan-Tung Vu, Thi Mai Thuong Tran, Anh-Hoang Truong, and Martin Steffen, 2012. A type system for finding upper resource bounds of multi-threaded programs with nested transactions. In Symposium on Information and Communication Technology 2012, SoICT ’12, Halong City, Quang Ninh, Viet Nam, August 23-24, 2012, pages 21-30. ABSTRACT A type system for counting logs of a minimal language with multithreaded and nested transactions We present a type system to estimate an upper bound for resource consumption of a multi-threaded, nested transactional memory program. The resource is abstracted as transaction logs. We build our type system for a core language with basic commands related to creating threads and transaction. Using the core language not only makes proving the soundness easier, it also allows us to extend the language with more features easier. Keywords: Type systems, resource bound, software transactional memory, static analysis, programming language. 93