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

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.
Nội dung trích xuất từ tài liệu:
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ảnJOURNAL OF SCIENCE OF HNUE DOI: 10.18173/2354-1075.2015-0055Educational Sci., 2015, Vol. 60, No. 7A, pp. 80-93This 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ế đồngbộ 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 giaodị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úctrong 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. Khilồ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 giaodị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ịchchư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 saocủ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 concủ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úngtô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ếtthú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ệtcho 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ơnnữ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ácNgà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.com80 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ảnbiế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ácluồ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áctrườ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 đếnkhả 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 để ướclượ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 trongnghiê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 chomộ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. Tuynhiê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. Trongnghiê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êntài nguyên sử dụng. Tofte và Talpin [13] sử ...