Luận án Tiến sĩ Công nghệ thông tin: Hệ thống kiểu để ước lượng tĩnh tài nguyên sử dụng của chương trình giao dịch

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

Thêm vào BST

Báo xấu

12
lượt xem 2
download

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

Luận án được hoàn thành với mục tiêu nhằm giúp người lập trình viết chương trình đơn giản hơn, tuy nhiên, nếu không quản lý tốt số log được sinh ra cũng như tài nguyên tiêu thụ của chương trình thì nguy cơ xảy ra các lỗi thiếu bộ nhớ hoặc các giao dịch phải chạy lại nhiều lần làm giảm hiệu suất của chương trình. Khi đó người lập trình sẽ không yên tâm để sử dụng cơ chế này.

Chủ đề:

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

Lưu

Nội dung Text: Luận án Tiến sĩ Công nghệ thông tin: Hệ thống kiểu để ước lượng tĩnh tài nguyên sử dụng của chương trình giao dịch

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN NGỌC KHẢI HỆ THỐNG KIỂU ĐỂ ƯỚC LƯỢNG TĨNH TÀI NGUYÊN SỬ DỤNG CỦA CHƯƠNG TRÌNH GIAO DỊCH LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN Hà Nội - 2022
ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ NGUYỄN NGỌC KHẢI HỆ THỐNG KIỂU ĐỂ ƯỚC LƯỢNG TĨNH TÀI NGUYÊN SỬ DỤNG CỦA CHƯƠNG TRÌNH GIAO DỊCH Chuyên ngành: Kỹ thuật phần mềm Mã số: 9480103.01 LUẬN ÁN TIẾN SĨ NGÀNH CÔNG NGHỆ THÔNG TIN NGƯỜI HƯỚNG DẪN KHOA HỌC: PGS.TS. TRƯƠNG ANH HOÀNG Hà Nội - 2022
Mục lục Trang Chương 1. GIỚI THIỆU. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.1. Đặt vấn đề . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2. Mục tiêu, đối tượng và phạm vi nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.1. Mục tiêu nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.2. Đối tượng và phạm vi nghiên cứu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3. Những đóng góp chính, ý nghĩa khoa học và thực tiễn . . . . . . . . . . . . . . . 5 1.4. Bố cục của luận án . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Chương 2. KIẾN THỨC NỀN TẢNG VÀ NGHIÊN CỨU LIÊN QUAN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2. Điều khiển tương tranh dựa trên khóa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.1. Khái niệm khóa. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.2. Kỹ thuật khóa đơn giản . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 2.2.3. Kỹ thuật khóa đọc, ghi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.4. Kỹ thuật Semaphore . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.2.5. Một số vấn đề trong kỹ thuật khóa . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3. Cơ chế bộ nhớ giao dịch phần mềm . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.1. Khái niệm và tính chất của giao dịch . . . . . . . . . . . . . . . . . . . . . . . . . . 15 2.3.2. Đặc điểm của chương trình STM. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.4. Hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 2.4.1. Khái niệm hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 2.4.2. Một số tính chất cơ bản của hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . 21 2.4.3. Ứng dụng và ý nghĩa của hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . 22 2.4.4. Hệ thống kiểu trong hình thức hóa ngôn ngữ . . . . . . . . . . . . . . . . . . . 23 2.5. Nghiên cứu liên quan . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 2.5.1. Tài nguyên tiêu thụ trong chương trình tuần tự . . . . . . . . . . . . . . . . 26 2.5.2. Tài nguyên tiêu thụ trong chương trình tương tranh. . . . . . . . . . . . 28 2.5.3. Tài nguyên tiêu thụ trong chương trình STM . . . . . . . . . . . . . . . . . . 31 i
2.5.4. Sử dụng hệ thống kiểu xác định biên tài nguyên tiêu thụ bởi chương trình STM . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 2.6. Tổng kết chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 Chương 3. ƯỚC LƯỢNG BIÊN TÀI NGUYÊN CHƯƠNG TRÌNH CỦA NGÔN NGỮ TỐI GIẢN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.1. Xác định số giao dịch tối đa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.1.1. Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 3.1.2. Ngôn ngữ giao dịch tối giản . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 3.1.2.1. Cú pháp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.1.2.2. Ngữ nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.1.3. Hệ thống kiểu tính số giao dịch tối đa. . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.1.3.1. Kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 3.1.3.2. Quy tắc kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45 3.1.3.3. Định kiểu chương trình ví dụ và thảo luận tính sắc của biên . . 47 3.1.3.4. Tính đúng của hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49 3.2. Xác định biên tài nguyên tiêu thụ của chương trình . . . . . . . . . . . . . . . . 53 3.2.1. Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 3.2.2. Ngôn ngữ giao dịch tối giản cải tiến . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.2.2.1. Cú pháp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 3.2.2.2. Ngữ nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.2.3. Hệ thống kiểu tìm biên tài nguyên tiêu thụ của chương trình . . . 60 3.2.3.1. Kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 60 3.2.3.2. Quy tắc kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 3.2.3.3. Định kiểu cho chương trình ví dụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64 3.2.3.4. Tính đúng của hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65 3.3. Tổng kết chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 Chương 4. TÍNH BỘ NHỚ TỐI ĐA CHO CHƯƠNG TRÌNH CỦA NGÔN NGỮ MỆNH LỆNH . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 68 4.2. Ví dụ minh họa. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 ii
4.3. Ngôn ngữ giao dịch với cấu trúc mệnh lệnh . . . . . . . . . . . . . . . . . . . . . . . . 71 4.3.1. Cú pháp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 71 4.3.2. Ngữ nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 73 4.4. Hệ thống kiểu tìm biên bộ nhớ cho các biến dùng chung . . . . . . . . . . . 76 4.4.1. Kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 76 4.4.2. Quy tắc kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 4.4.3. Tính đúng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 4.4.4. Định kiểu cho chương trình ví dụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83 4.5. Công cụ suy diễn kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.5.1. Định nghĩa kiểu dữ liệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 84 4.5.2. Hàm chính. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 4.5.3. Hàm rút gọn. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85 4.5.4. Hàm hợp hai chuỗi . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 86 4.5.5. Hàm đồng kết thúc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 4.5.6. Hàm chuyển dạng. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 4.5.7. Hàm chọn . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90 4.6. Hệ thống kiểu tích hợp xác định biên bộ nhớ cấp phát cho các biến dùng chung . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 4.6.1. Kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 91 4.6.2. Quy tắc định kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 92 4.6.3. Đặc điểm của hệ thống kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 99 4.6.4. Định kiểu chương trình ví dụ và thảo luận tính sắc của biên . . 112 4.7. Tổng kết chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 117 Chương 5. XÁC ĐỊNH BỘ NHỚ GIAO DỊCH TỐI ĐA CHO CHƯƠNG TRÌNH CỦA NGÔN NGỮ HƯỚNG ĐỐI TƯỢNG 118 5.1. Giới thiệu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 118 5.2. Ví dụ minh họa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 5.2.1. Phân tích hành vi của chương trình . . . . . . . . . . . . . . . . . . . . . . . . . . . 120 5.2.2. Phân tích bộ nhớ sử dụng bởi chương trình . . . . . . . . . . . . . . . . . . . 124 iii
5.3. Ngôn ngữ giao dịch với cấu trúc hướng đối tượng . . . . . . . . . . . . . . . . . 126 5.3.1. Cú pháp . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 126 5.3.2. Ngữ nghĩa . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 5.4. Hệ thống kiểu tích hợp tìm biên bộ nhớ giao dịch . . . . . . . . . . . . . . . . . 133 5.4.1. Kiểu. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 133 5.4.2. Quy tắc kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 134 5.4.3. Định kiểu cho chương trình ví dụ . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 141 5.4.4. Tính đúng . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 143 5.5. Tổng kết chương . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 144 Chương 6. KẾT LUẬN . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 6.1. Những kết quả đạt được . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 145 6.2. Những hạn chế và hướng nghiên cứu tiếp theo . . . . . . . . . . . . . . . . . . . . 147 Phụ lục: KIỂM THỬ CÔNG CỤ SUY DIỄN KIỂU . . . . . . . . . . . 159 iv
Danh sách hình vẽ 2.1 Sơ đồ các trạng thái của giao dịch. . . . . . . . . . . . . . . . . . . . . 16 2.2 Hệ thống kiểu liên kết với quá trình biên dịch. . . . . . . . . . . . . . 25 3.1 Mô tả hành vi của chương trình trong ví dụ. 3.1 . . . . . . . . . . . . 36 3.2 Đồng kết thúc các luồng. . . . . . . . . . . . . . . . . . . . . . . . . . . 46 3.3 Mô tả hành vi của chương trình ví dụ 3.3. . . . . . . . . . . . . . . . . 54 4.1 Mô tả hành vi hoạt động của ví dụ 4.1. . . . . . . . . . . . . . . . . . 71 4.2 Các giao dịch lồng nhau. . . . . . . . . . . . . . . . . . . . . . . . . . . 95 4.3 Đồng kết thúc các luồng song song (trường hợp 1). . . . . . . . . . . 97 4.4 Đồng kết thúc các luồng song song (trường hợp 2). . . . . . . . . . . 97 4.5 Cây suy diễn kiểu cho đoạn chương trình e10 trong Đoạn mã 4.10. . 113 29 4.6 Hành vi của Đoạn chương trình trong Đoạn mã 4.10 . . . . . . . . . 114 4.7 Cây suy diễn kiểu của chương trình trong Đoạn mã 4.10. . . . . . . . 116 5.1 Mô phỏng hành vi của chương trình trong đoạn mã ví dụ 5.1 . . . . 126 5.2 Giao dịch lồng nhau . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 5.3 Các hành phần tuần tự. . . . . . . . . . . . . . . . . . . . . . . . . . . . 138 5.4 Các luồng song song. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 139 5.5 Hợp hai luồng song song. . . . . . . . . . . . . . . . . . . . . . . . . . . 139 5.6 Đồng kết thúc các luồng song song. . . . . . . . . . . . . . . . . . . . . 140 v
Danh sách bảng 3.1 Cú pháp của ngôn ngữ STM tối giản . . . . . . . . . . . . . . . . . . . 38 3.2 Ngữ nghĩa cục bộ của ngôn ngữ STM tối giản . . . . . . . . . . . . . 39 3.3 Ngữ nghĩa giao dịch và luồng của ngôn ngữ STM tối giản . . . . . . 40 3.4 Quy tắc định kiểu cho chương trình STM tối giản . . . . . . . . . . . 45 3.5 Cú pháp của ngôn ngữ giao dịch tối giản cải tiến . . . . . . . . . . . . 57 3.6 Ngữ nghĩa của ngôn ngữ giao dịch tối giản cải tiến . . . . . . . . . . 58 3.7 Quy tắc định kiểu chương trình STM tối giản cải tiến . . . . . . . . . 62 4.1 Cú pháp của ngôn ngữ giao dịch cấu trúc mệnh lệnh . . . . . . . . . 73 4.2 Ngữ nghĩa của ngôn ngữ giao dịch cấu trúc mệnh lệnh . . . . . . . . 74 4.3 Quy tắc kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 80 4.4 Quy tắc kiểu của hệ thống kiểu tích hợp . . . . . . . . . . . . . . . . . 92 5.1 Cú pháp của ngôn ngữ STM hướng đối tượng . . . . . . . . . . . . . . 127 5.2 Ngữ nghĩa của ngôn ngữ STM hướng đối tượng . . . . . . . . . . . . 129 5.3 Quy tắc định kiểu . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 135 vi
Thuật ngữ và từ viết tắt Từ viết tắt Từ gốc Giải nghĩa - Tạm dịch ACID Atomicity, Consistency, Iso- Tính chất của một giao dịch: tính lation and Durability nguyên tố, tính nhất quán, tính độc lập, và tính bền vững CFG Control Flow Graph Luồng điều khiển CPU Central Processing Unit Bộ xử lý trung tâm CR Cost Relations Biểu thức mô tả mối quan hệ chi phí của chương trình DAG Directed Acyclic Graph Đồ thị có hướng phi chu trình DFG Distributed Flow Graph Biểu đồ luồng phân tán HTM Hardware Transactional Bộ nhớ giao dịch phần cứng Memory HyTM Hybrid Transactional Mem- Phương pháp lai giữa bộ nhớ giao ory dịch phần cứng và phần mềm IoT Internet of Things Internet vạn vật MB Megabyte Đơn vị thông tin ML Machine languague Ngôn ngữ máy SACO Static Analyzer for Concur- Máy phân tích tĩnh cho các đối rent Objects tượng tương tranh STAMP Stanford Transactional Một thư viện sử dụng cơ chế bộ Applications for Multi- nhớ giao dịch phần mềm Processing STM Software Transactional Bộ nhớ giao dịch phần mềm Memory TFJ Transactional Featherweight Ngôn ngữ giao dịch Java tối giản Java vii
Lời cam đoan Tôi xin cam đoan đây là công trình nghiên cứu do tôi thực hiện dưới sự hướng dẫn của PGS.TS. Trương Anh Hoàng tại bộ môn Công nghệ phần mềm, khoa Công nghệ thông tin, trường Đại học Công nghệ, Đại học Quốc gia Hà Nội. Các số liệu và kết quả trình bày trong luận án là trung thực, chưa được công bố bởi bất kỳ tác giả nào hay ở bất kỳ công trình nào khác. Tác giả Nguyễn Ngọc Khải viii
Lời cảm ơn Trước tiên tôi xin gửi lời cảm ơn chân thành và sâu sắc đến PGS.TS. Trương Anh Hoàng - người đã hướng dẫn, khuyến khích, truyền cảm hứng, chỉ bảo và tạo cho tôi những điều kiện tốt nhất từ khi bắt đầu làm nghiên cứu sinh đến khi hoàn thành luận án này. Tôi xin chân thành cảm ơn các thầy cô giáo khoa Công nghệ thông tin, trường Đại học Công nghệ, Đại học Quốc gia Hà Nội, đặc biệt là các thầy cô trong bộ môn Công nghệ phần mềm đã tận tình đào tạo, cung cấp cho tôi những kiến thức vô cùng quý giá, đã tạo điều kiện tốt nhất cho tôi về môi trường làm việc trong quá trình học tập, nghiên cứu tại Trường. Đồng thời tôi xin chân thành cảm ơn các đồng nghiệp trong trường Đại học Tài nguyên và Môi trường Hà Nội đã tạo mọi điều kiện, bố trí thời gian tốt nhất dành cho tôi trong quá trình làm nghiên cứu sinh. Cuối cùng, tôi xin chân thành cảm ơn những người thân trong gia đình cùng toàn thể bạn bè đã luôn giúp đỡ, động viên tôi những lúc gặp phải khó khăn trong quá trình học tập và nghiên cứu. ix
Tóm tắt Trong lập trình tương tranh, người lập trình thường sử dụng cơ chế dựa trên khóa (lock based) để đồng bộ giữa các luồng. Tuy nhiên, cơ chế này tiềm ẩn nhiều lỗi về khóa như lỗi khóa sống (livelock), lỗi khóa chết (deadlock) và người lập trình phải quan tâm tới việc quản lý các khóa. Vì vậy, người lập trình thường gặp nhiều khó khăn khi sử dụng cơ chế này. Cơ chế Bộ nhớ giao dịch phần mềm (Software Transactional Memory - STM) là một lựa chọn thay thế cho cơ chế dựa trên khóa để đồng bộ giữa các luồng. Cơ chế này giúp khắc phục những lỗi do cơ chế dựa trên khóa gây ra, giúp người lập trình viết chương trình đơn giản hơn. Theo cơ chế STM, khi một luồng hoặc một giao dịch cần sử dụng các đối tượng dùng chung, chúng sẽ nhân bản các đối tượng đó thành các bản sao (gọi là các log) để sử dụng độc lập. Khi các luồng đồng bộ, các log này sẽ được so sánh với bản gốc của nó, nếu không có mâu thuẫn, chúng sẽ được cập nhật vào bản gốc và các log được giải phóng. Ngược lại, nếu có mâu thuẫn (đối tượng gốc đã bị thay đổi bởi các giao dịch khác), giao dịch sẽ phải thực hiện lại (rollback) hoặc bị hủy bỏ (abort). Do cơ chế tạo bản sao các đối tượng dùng chung dẫn đến chương trình sử dụng cơ chế STM tiêu thụ nhiều tài nguyên bộ nhớ hơn các phương pháp truyền thống. Thêm nữa, khi chương trình tạo ra quá nhiều log, các giao dịch có nguy cơ phải thực hiện lại nhiều lần do các log bị xung đột, dẫn đến giảm hiệu suất của chương trình. Vì vậy, khi sử dụng cơ chế này, người lập trình chỉ yên tâm khi họ kiểm soát được việc sử dụng tài nguyên bộ nhớ và số lượng log được tạo ra của chương trình. Đặc biệt, điều này rất quan trọng đối với lập trình nhúng, lập trình với các thiết bị IoT, khi mà các thiết bị này có dung lượng bộ nhớ hạn chế. Mục tiêu nghiên cứu của luận án là phân tích các chương trình tương tranh, hỗ trợ cấu trúc giao dịch lồng nhau, và sử dụng cơ chế STM để xử lý vấn đề đồng bộ giữa các luồng (gọi tắt là chương trình giao dịch hay chương trình STM ), từ đó xây dựng một hệ thống kiểu với mục đích ước lượng tĩnh tài nguyên bộ nhớ tối đa mà các chương trình STM cần sử dụng. Hệ thống kiểu này khi được hoàn thiện có thể tích hợp vào các trình soạn thảo mã nguồn hoặc các trình biên dịch để cung cấp thông tin về lượng tài nguyên bộ nhớ mà chương trình cần sử dụng, từ đó giúp người lập trình kiểm soát được mức tiêu thụ tài nguyên bộ nhớ của chương trình và đưa ra các phương án để tối ưu chương trình. x
Để tập trung trình bày rõ những tính chất của cơ chế STM và giải quyết bài toán một cách tổng quát, luận án đưa ra những ngôn ngữ cốt lõi hoạt động theo cơ chế STM và lược bỏ hoặc đơn giản hóa một số tính chất của ngôn ngữ thực tế như tính kế thừa trong lập trình hướng đối tượng, vòng lặp vô hạn, hay các vấn đề về xung đột giữa các giao dịch. Từ đó, luận án xây dựng các hệ thống kiểu để tính toán trên những chương trình được viết bằng các ngôn ngữ này để đưa ra biên tài nguyên bộ nhớ mà chương trình cần sử dụng. Do sự phức tạp của bài toán đặt ra nên luận án chia bài toán thành nhiều bước để thực hiện như sau: - Luận án xây dựng một ngôn ngữ giao dịch tối giản và một hệ thống kiểu để xác định tài nguyên tiêu thụ tối đa của chương trình. Tại bước này, luận án xây dựng một ngôn ngữ đa luồng hoạt động theo cơ chế STM. Ngôn ngữ này chỉ gồm những lệnh cơ bản nhất như tạo luồng, mở, đóng giao dịch (gọi ngôn ngữ này là ngôn ngữ giao dịch tối giản). Sau đó, luận án xây dựng một hệ thống kiểu để xác định số giao dịch tối đa của các chương trình viết bằng ngôn ngữ này. Lưu ý rằng số giao dịch tối đa chưa phải là lượng tài nguyên tối đa cần sử dụng của chương trình. Hệ thống kiểu này có các quy tắc đơn giản, thuận lợi cho việc cài đặt, mở rộng, phát triển, và chứng minh các tính chất của nó. Sau đó, luận án tiến hành mở rộng ngôn ngữ bằng cách bổ sung thêm vào mỗi giao dịch một tham số thể hiện lượng tài nguyên mà giao dịch cần sử dụng. Những tham số này không phải do người lập trình cung cấp mà chúng sẽ được tổng hợp từ các câu lệnh, các khai báo trong các giao dịch. Đồng thời, luận án xây dựng một hệ thống kiểu để xác định tài nguyên tối đa mà chương trình cần sử dụng dựa trên các tham số này. Ngôn ngữ và hệ thống kiểu trong phần này mang tính tổng quát và là nền tảng cho các nghiên cứu tiếp theo. Sau khi hoàn thành ngôn ngữ và hệ thống kiểu tổng quát này, luận án tiếp tục thực hiện các bước tiếp theo để cải tiến ngôn ngữ và hệ thống kiểu để gần với thực tế hơn. - Luận án mở rộng ngôn ngữ giao dịch và cải tiến các hệ thống kiểu để ước lượng tài nguyên tiêu thụ cho các biến dùng chung của chương trình. Đây là những thành phần sẽ bị nhân bản bởi cơ chế STM. Trong bước này, ngôn ngữ được mở rộng với cấu trúc mệnh lệnh có các khai báo biến, các câu lệnh điều kiện, câu lệnh vòng lặp cụ thể gần với ngôn ngữ thực tế. Từ đó, luận án xây dựng một hệ thống kiểu để xác định bộ nhớ xi
cấp phát cho các biến dùng chung của những chương trình viết bởi ngôn ngữ này. Đồng thời hệ thống kiểu được cải tiến để có khả năng tích hợp. Nghĩa là chúng có thể định kiểu cho những đoạn chương trình khác nhau sau đó tích hợp lại thành kiểu của cả chương trình. - Ngôn ngữ được mở rộng với cấu trúc hướng đối tượng, cải tiến cơ chế STM, và hệ thống kiểu được cải tiến để ước lượng bộ nhớ giao dịch của chương trình. Tại bước này, luận án tiếp tục mở rộng ngôn ngữ để trở thành ngôn ngữ giao dịch với cấu trúc hướng đối tượng, đồng thời cải tiến cơ chế STM để chương trình sử dụng bộ nhớ hiệu quả hơn. Cùng với đó, luận án xây dựng một hệ thống kiểu tương ứng để xác định biên bộ nhớ cấp phát cho các đối tượng dùng chung của các giao dịch (gọi là biên bộ nhớ giao dịch). Kết quả của nghiên cứu này là một ngôn ngữ và một hệ thống kiểu gần với thực tế nhất. - Ngoài những kết quả chính là những ngôn ngữ và hệ thống kiểu ở trên, luận án cũng đã thực hiện cài đặt các quy tắc kiểu để được công cụ có thể suy ra kiểu của một chương trình hợp lệ. Các công cụ này được xây dựng bằng phương pháp lập trình hàm và đã được thông qua với một số ca kiểm thử do luận án đề xuất. Kết quả của nghiên cứu này không chỉ có ý nghĩa trong việc giải quyết bài toán ước lượng tài nguyên bộ nhớ của chương trình STM, mà chúng còn đóng góp cho cộng đồng nghiên cứu về lý thuyết kiểu những hệ thống kiểu mới có ý nghĩa. Những hệ thống kiểu này có thể làm nền tảng để chúng ta mở rộng, phát triển để giải quyết những bài toán khác, chẳng hạn như xác định số gas yêu cầu bởi các hợp đồng thông minh trong Ethereum, xác định tài nguyên CPU, tài nguyên đường truyền mạng, hay ước lượng thời gian cần thiết để một chương trình hoàn thành một công việc. xii
Chương 1 GIỚI THIỆU 1.1. Đặt vấn đề Ngày nay, những thiết bị được trang bị bộ vi xử lý đa lõi trở nên phổ biến, vì vậy việc phát triển những phần mềm tương tranh để khai thác hiệu quả các hệ thống phần cứng này cũng đang rất phát triển. Tuy nhiên, việc phát triển các phần mềm tương tranh đòi hỏi nhiều kỹ thuật phức tạp hơn so với phát triển các phần mềm hoạt động theo cơ chế tuần tự, trong đó việc đồng bộ giữa các luồng có thể được xem là một trong những kỹ thuật phức tạp nhất của các hệ thống phần mềm này. Thông thường người lập trình thường sử dụng cơ chế dựa trên khóa (lock based) để đồng bộ các luồng [87]. Tuy nhiên, cơ chế đồng bộ dựa trên khóa có thể gây ra nhiều lỗi nghiêm trọng như lỗi khóa sống (livelock), lỗi khóa chết (deadlock), và những lỗi tiềm ẩn khác về khóa. Ngoài ra, người lập trình còn phải quan tâm tới việc quản lý các khóa. Điều này gây ra nhiều khó khăn, phức tạp cho người lập trình. Trong một số trường hợp, người lập trình sử dụng cơ chế Semaphore [35] để quản lý việc truy cập các tài nguyên dùng chung giữa các luồng, tuy nhiên cơ chế này cũng gặp một số khó khăn tương tự như cơ chế dựa trên khóa. Để giúp người lập trình viết chương trình đơn giản hơn, một số giải pháp thay thế cho cơ chế dựa trên khóa đã được đề xuất, trong đó cơ chế bộ nhớ giao dịch là một giải pháp nhiều hứa hẹn [59, 46, 42]. Nền tảng để thực hiện bộ nhớ giao dịch có thể được thực hiện hoàn toàn thông qua phần mềm (Software Transactional Memory - STM) [84, 45, 82, 83], hoặc hoàn toàn thông qua các thành phần phần cứng (Hardware Transactional Memory - HTM) [13, 72, 27, 80], hoặc kết hợp cả phần cứng và phần mềm - phương pháp lai (Hybrid Transactional Memory - HyTM) [26, 34, 65, 86, 88]. Tuy nhiên, một số nghiên cứu đã chỉ ra rằng, cuộc cách mạng về tương tranh chủ yếu là cuộc cách mạng phần mềm [87]. Vấn đề không phải là phát triển các hệ thống phần cứng đa lõi, mà vấn đề chính là làm thế nào để lập trình hiệu quả các chương trình theo cách cho phép các ứng dụng tận dụng được sự tăng trưởng liên tục theo cấp số nhân về hiệu suất của CPU. Trong nghiên cứu này, 1
Chương 1. Giới thiệu 2 luận án tập trung nghiên cứu lớp những chương trình tương tranh hỗ trợ cấu trúc giao dịch lồng nhau, và sử dụng cơ chế STM để điều khiển việc đồng bộ giữa các luồng, các giao dịch. Luận án gọi các chương trình này là chương trình giao dịch hay ngắn gọn hơn là chương trình STM. Cơ chế STM gần đây được trang bị cho một số ngôn ngữ lập trình tương tranh hiện đại như để người lập trình có thể sử dụng thay thế cho cơ chế đồng bộ dựa trên khóa [42]. Điểm nổi bật trong các ngôn ngữ này đó là được trang bị những tính năng giao dịch đa luồng và lồng nhau. Đây là những tính năng tiên tiến, tạo nhiều thuận lợi cho người lập trình. Giao dịch đa luồng có nghĩa là ở trong một giao dịch chúng ta có thể khởi tạo nhiều luồng. Giao dịch lồng nhau ở đây đặc biệt ở chỗ một giao dịch có thể chứa một hoặc nhiều giao dịch ở trong một luồng con, và luồng con phải đồng bộ với giao dịch của luồng cha khi giao dịch thực hiện cam kết (commit). Khi một giao dịch cam kết, các luồng con ở trong giao dịch đó cũng phải cùng cam kết. Để các luồng/giao dịch chạy được độc lập, không phải chờ đợi nhau, mỗi luồng/giao dịch sẽ tạo ra các bản sao các thành phần dùng chung (gọi là các log), và thao tác trên các bản sao đó. Sau khi hoàn thành giao dịch, chúng sẽ đồng bộ các log và các giá trị gốc của nó. Nếu không có xung đột, giao dịch sẽ được hoàn thành, ngược lại giao dịch sẽ phải thực hiện lại (rollback), hoặc bị hủy bỏ (abort). Cơ chế tạo ra các bản sao của các thành phần dùng chung làm cho chương trình STM tiêu thụ nhiều tài nguyên bộ nhớ hơn các chương trình truyền thống khác. Điều này có thể dẫn đến các lỗi thiếu tài nguyên bộ nhớ khi thực thi chương trình. Hơn nữa, nếu quá nhiều log được tạo ra đồng thời thì nguy cơ xung đột sẽ tăng cao, nhiều giao dịch sẽ phải thực hiện lại hoặc bị hủy bỏ. Điều này làm giảm đáng kể hiệu suất của chương trình. Mục đích nghiên cứu của luận án là đưa ra được phương pháp để giúp người lập trình ước lượng tĩnh số log tối đa cùng tồn tại và tài nguyên tối đa cần sử dụng của các chương trình đa luồng hoạt động theo cơ chế STM. Từ đó, người lập trình có thể tối ưu chương trình của mình để nâng cao hiệu suất của chương trình và sử dụng tài nguyên hiệu quả hơn, nhằm tiết kiệm tài nguyên, hạn chế các lỗi do thiếu tài nguyên khi thực thi chương trình. Do sự phức tạp của bài toán đặt ra nên luận án chia bài toán thành nhiều bước để giải quyết. Ban đầu, luận án giải quyết bài toán xác định số lượng log lớn nhất cùng tồn tại trong một thời điểm. Từ đây chúng ta đã có thông tin sơ 2
Chương 1. Giới thiệu 3 bộ về bộ nhớ log sử dụng. Làm mịn thêm kích thước của các log này dựa trên thông tin về số lượng và kiểu của các biến hoặc các đối tượng trên các log, chúng ta có được thông tin cụ thể về bộ nhớ sử dụng của chương trình. Đã có nhiều nghiên cứu khác nhau về thiết kế, ứng dụng của cơ chế STM [59, 99], tuy nhiên, các nghiên cứu thường chỉ tập trung vào các vấn đề hiệu suất thực hiện của chương trình mà bỏ qua các yếu tố quan trọng về sự tiêu tốn tài nguyên, năng lượng của các hệ thống STM. Chúng tôi cho rằng, nếu STM trở thành chủ đạo, những yếu tố về tài nguyên, năng lượng cần cho hệ thống cũng rất cần được quan tâm nghiên cứu. Điều này đặc biệt đúng đối với các hệ thống nhúng, bởi vì trong các hệ thống nhúng, tài nguyên, năng lượng tiêu thụ liên quan chặt chẽ đến tuổi thọ pin, hay các trung tâm dữ liệu, nơi mà tài nguyên, năng lượng tiêu hao đóng góp đáng kể vào chi phí hoạt động, và thậm chí cả trong môi trường máy tính để bàn [17]. Do đó việc ước lượng tài nguyên, năng lượng tiêu thụ là một bài toán quan trọng trong hầu hết các hệ thống này. Tính mới và ý nghĩa khoa học của nghiên cứu này không chỉ ở bài toán đặt ra mà còn ở giải pháp mà luận án đưa ra để giải quyết bài toán. Các nghiên cứu liên quan chỉ chủ yếu giải quyết cho chương trình tuần tự hoặc song song độc lập của các luồng. Sự phức tạp của bài toán đặt ra ở đây đó là các luồng không chạy độc lập hoàn toàn với nhau mà khi một giao dịch cam kết thì các luồng con trong giao dịch cũng phải cùng cam kết. Hệ thống kiểu của luận án có cấu trúc giàu thông tin và có thể áp dụng được cho nhiều hệ thống song song có đồng bộ tương tự. Giải pháp sử dụng hệ thống kiểu tĩnh của luận án cũng giúp việc xác định tài nguyên đảm bảo tính đúng mà không cần chạy chương trình. Việc này có ý nghĩa khoa học đối với lĩnh vực phương pháp hình thức trong phát triển phần mềm. Tính thời sự và sự cần thiết của nghiên cứu này có thể thấy rõ trong ngữ cảnh phát triển phần mềm trên các thiết bị di động ngày nay. Thứ nhất, ngày càng có nhiều thiết bị di động sử dụng bộ xử lý đa nhân. Việc viết chương trình đa luồng để khai thác các nhân này đang là thực tế đặt ra. Các ngôn ngữ hiện nay sử dụng cơ chế đồng bộ dựa trên khóa gây khó khăn cho người lập trình, và gây các lỗi khóa chết, khóa sống khó có thể kiểm soát được. Cơ chế bộ nhớ giao dịch sẽ giải phóng người người lập trình khỏi các khóa/đồng bộ, giúp việc lập trình đơn giản hơn và không lo lỗi về khóa. Bộ nhớ giao dịch không thay thế hoàn toàn cơ chế dựa trên khóa, mà tùy theo bài toán thực tế, người lập trình lựa chọn giải pháp cho phù hợp. Mặc dù 3
Chương 1. Giới thiệu 4 cơ chế đồng bộ dựa trên khóa đang được sử dụng phổ biến do ưu điểm chúng đã được phát triển từ rất lâu, quen thuộc với người lập trình, và được hỗ trợ bởi nhiều ngôn ngữ lập trình. Tuy nhiên, cơ chế bộ nhớ giao dịch với nhiều ưu điểm vượt trội như đã phân tích ở trên sẽ là một lựa chọn tốt cho người lập trình. Bên cạnh đó, cơ chế bộ nhớ giao dịch cũng có những hạn chế, đó là việc tiêu thụ nhiều tài nguyên, nguy cơ phải thực hiện lại hoặc hủy bỏ giao dịch cao làm giảm hiệu suất của chương trình. Vì vậy nếu không kiểm soát tốt số log chương trình tạo ra và tài nguyên chúng sử dụng thì người lập trình không sẵn sàng để sử dụng chúng. 1.2. Mục tiêu, đối tượng và phạm vi nghiên cứu 1.2.1. Mục tiêu nghiên cứu Mặc dù cơ chế STM có nhiều ưu điểm, giúp người lập trình viết chương trình đơn giản hơn, tuy nhiên, nếu không quản lý tốt số log được sinh ra cũng như tài nguyên tiêu thụ của chương trình thì nguy cơ xảy ra các lỗi thiếu bộ nhớ hoặc các giao dịch phải chạy lại nhiều lần làm giảm hiệu suất của chương trình. Khi đó người lập trình sẽ không yên tâm để sử dụng cơ chế này. Vì vậy, với mục tiêu giúp người lập trình kiểm soát số log chương trình tạo ra cũng như tài nguyên tiêu thụ của chương trình, luận án đặt ra hai mục tiêu chính đó là: - Thứ nhất, đưa ra được phương pháp tin cậy để ước lượng tĩnh (không cần chạy chương trình) cận trên tài nguyên bộ nhớ cần sử dụng cho các thành phần dùng chung của các chương trình giao dịch. Phương pháp đề xuất cần mang tính tổng quát, làm nền tảng để có thể cải tiến để ứng dụng được cho nhiều ngôn ngữ trong thực tế, đồng thời có thể mở rộng cho các bài toán xác định các loại tài nguyên khác mà chương trình cần sử dụng. - Thứ hai, xây dựng được công cụ để ước lượng biên tài nguyên bộ nhớ cần sử dụng của chương trình. Công cụ này khi được hoàn thiện có thể tích hợp vào các trình soạn thảo, hoặc trình biên dịch để đưa ra các thông tin về số giao dịch tối đa, biên tài nguyên bộ nhớ cần sử dụng cho người lập trình, giúp người lập trình tối ưu chương trình của họ. 1.2.2. Đối tượng và phạm vi nghiên cứu Luận án sẽ tập trung nghiên cứu lớp các ngôn ngữ hỗ trợ cấu trúc đa luồng, có các giao dịch đan xen lồng nhau, và sử dụng cơ chế STM trong việc đồng bộ giữa các luồng, các giao dịch. 4
Chương 1. Giới thiệu 5 Do tính phức tạp của bài toán đặt ra và để tập trung mô tả rõ vấn đề xác định biên tài nguyên bộ nhớ cấp phát cho các đối tượng bị nhân bản bởi cơ chế STM, luận án sẽ tập trung mô tả các tính chất của ngôn ngữ có liên quan đến việc cấp phát, giải phóng bộ nhớ của chương trình do cơ chế STM gây ra. Một số tính chất khác của ngôn ngữ như tính kế thừa trong lập trình hướng đối tượng, vòng lặp vô hạn, hay vấn đề xung đột giữa các giao dịch, vấn đề ưu tiên thứ tự xử lý các giao dịch dự kiến sẽ tiếp tục được thực hiện trong các nghiên cứu tiếp theo trong tương lai. Nghiên cứu này thiên về lý thuyết và nền tảng toán học, làm nền tảng cho các nghiên cứu tiếp theo. Trong phạm vi của luận án, việc cài đặt công cụ sẽ dừng ở mức cài đặt các công cụ suy diễn kiểu cho chương trình. Chúng tôi kỳ vọng, trong tương lai, khi có thêm thời gian, nguồn lực, trên cơ sở sản phẩm của luận án, nhóm nghiên cứu sẽ phát triển được các công cụ hữu ích, ứng dụng hiệu quả trong thực tế. 1.3. Những đóng góp chính, ý nghĩa khoa học và thực tiễn Những đóng góp chính của luận án bao gồm hai hệ thống kiểu để ước lượng tĩnh cận trên tài nguyên cần sử dụng cho các thành phần dùng chung và một công cụ để suy diễn kiểu cho chương trình STM: - Hệ thống kiểu thứ nhất được xây dựng với các quy tắc đơn giản hơn, thuận lợi để mở rộng và cài đặt. Hệ thống kiểu này yêu cầu một chương trình hoàn thiện (nghĩa là một chương trình đã được viết xong và hợp lệ) thì mới có thể định kiểu được. Chúng phù hợp để định kiểu cho các chương trình nhỏ, được viết bởi số ít người. - Hệ thống kiểu thứ hai có khả năng định kiểu linh hoạt hơn. Chúng có thể định kiểu cho những thành phần bất kỳ trong chương trình mà không cần phải là một chương trình hoàn chỉnh, sau đó tích hợp lại để được kiểu của toàn bộ chương trình. Tính chất này được gọi là tính tích hợp, một trong những đặc điểm thường thấy của các hệ thống kiểu. Hệ thống kiểu này phù hợp để định kiểu cho những chương trình lớn, được viết bởi nhiều người. - Công cụ suy diễn kiểu được cài đặt dựa trên các quy tắc kiểu đã đề xuất, cho phép định kiểu cho một chương trình STM. Ý nghĩa của luận án không chỉ ở việc giải quyết bài toán ước lượng tài nguyên bộ nhớ của chương trình, mà luận án còn có ý nghĩa trong việc góp phần phát 5
Chương 1. Giới thiệu 6 triển lĩnh vực nghiên cứu về lý thuyết kiểu trong phương pháp hình thức trong công nghệ phần mềm. Cụ thể, luận án đã đóng góp cho cộng đồng nghiên cứu những bộ quy tắc kiểu với mục đích chính để giúp người lập trình kiểm soát được tài nguyên chương trình cần sử dụng. Bộ quy tắc này là nền tảng để chúng ta có thể mở rộng, phát triển cho các mục đích khác, chẳng hạn như xác định tài nguyên CPU, độ phức tạp thời gian, số gas tiêu thụ trong các hợp đồng thông minh trong Ethereum [11, 28]. Ngoài ra, công cụ suy diễn kiểu khi được tích hợp vào các trình soạn thảo cũng góp phần tác động tới suy nghĩ của người lập trình trong việc tối ưu thuật toán để sử dụng tiết kiệm tài nguyên trong quá trình phát triển chương trình. Những nghiên cứu hiện tại chủ yếu giải quyết cho chương trình tuần tự hoặc song song nhưng các luồng hoạt động độc lập. Chúng chỉ là những trường hợp riêng trong bài toán đặt ra của nghiên cứu này. Những nghiên cứu cho các chương trình đa luồng sử dụng cơ chế STM chủ yếu được thực hiện theo phương pháp động, nghĩa là thực thi chương trình trong những ngôn ngữ cụ thể để thực hiện việc so sánh, đánh giá. Những phương pháp này chỉ cho kết quả gần đúng và yêu cầu phải có chương trình hoàn thiện để thực hiện thử nghiệm. Hệ thống kiểu trong luận án có cấu trúc giàu thông tin và có thể áp dụng được cho nhiều chương trình tương tranh có cách thức đồng bộ tương tự. Giải pháp sử dụng hệ thống kiểu của luận án cũng giúp việc xác định tài nguyên đảm bảo tính đúng mà không cần chạy chương trình. Tính thời sự và sự cần thiết của nghiên cứu này có thể thấy rõ trong ngữ cảnh phát triển phần mềm trên các thiết bị đa nhân ngày nay. Ngày càng có nhiều thiết bị sử dụng bộ xử lý đa nhân. Việc viết chương trình đa luồng để khai thác các thiết bị này đang là thực tế đặt ra. Cơ chế STM là một cơ chế mạnh, giúp người lập trình viết các chương trình giao dịch đa luồng đơn giản hơn. Tuy nhiên, như đã trình bày ở trên, với cơ chế này người lập trình chỉ yên tâm khi kiểm soát được tài nguyên sử dụng và số log tối đa được tạo ra bởi chương trình. Đặc biệt, điều này có ý nghĩa quan trọng đối với lập trình nhúng, lập trình cho các thiết bị IoT, khi mà tài nguyên bộ nhớ hạn chế, cũng như sự tiêu tốn tài nguyên liên quan trực tiếp đến tuổi thọ của pin. Vì vậy, kết quả của luận án là một giải pháp giúp cho người lập trình yên tâm sử dụng cơ chế STM hơn, giúp cho cơ chế STM phổ biến hơn trong thực tế. 6