ĐẠ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
