tailieunhanh - 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. | 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: 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 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 .