Thạc Sĩ Tính cận trên bộ nhớ log của chương trình sử dụng giao dịch

MỞ ĐẦU
Tính cấp thiết của đề tài
Cùng với sự phát triển như v b o của khoa học công nghệ, các vi x lý hiện đ i ngày càng thể hiện sức m nh qua nhiều nhân (core) với tốc độ x lý ngày càng cao. Có được như vậy là do bên trong các vi x lý này được thiết kế các luồng (thread) có khả năng ch y và x lý song song. Trước đ y để lập trình đa luồng, người ta s dụng cơ chế đồng bộ (synchronization) dựa trên kh a (lock) để p đặt giới h n về quyền truy cập tài nguyên trong một môi trường khi có nhiều luồng thực thi.Tuy nhiên, khi áp dụng phương ph p này thường nảy sinh các vấn đề như khóa chết (deadlock) hoặc các lỗi tiềm tàng
Software Transactional Memory (STM- bộ nhớ giao dịch phần mềm) [8] là một giải ph p đơn giản hơn nhưng vô c ng m nh mẽ mà có thể giải quyết được hầu hết các vấn đề trên. N đ thay thế hoàn toàn giải ph p c trong việc truy cập bộ nhớ dùng chung. STM giao tiếp với bộ nhớ thông qua các giao dịch. Các giao dịch này cho phép tự do đọc ghi để chia sẻ các biến và một vùng nhớ gọi là log sẽ được s dụng để ghi l i các ho t động này cho tới khi kết thúc giao dịch.
Một trong những mô hình giao dịch phức t p s dụng STM là mô hình giao dịch lồng và đa luồng (nested and multi-threaded transaction) [5]. Trong quá trình thực thi của c c chương tr nh giao dịch lồng và đa luồng, khi các luồng mới được sinh ra hoặc một giao dịch được bắt đầu, các vùng bộ nhớ gọi là log sẽ được cấp phát. Các log này d ng để lưu l i bản sao của các biến dùng chung, nhờ vậy mà các luồng trên có thể s dụng các biến này một c ch độc lập.
Vấn đề đặt ra ở đ y là t i thời điểm chương tr nh ch y liệu lượng bộ nhớ cần cấp ph t cho c c log c vượt quá tài nguyên bộ nhớ của máy, hay chương tr nh c thể ch y một c ch trơn tru mà không gặp phải bất kỳ lỗi nào như hết bộ nhớ. Chính vì vậy, việc x c định cận trên của bộ nhớ ở thời điểm ch y chương tr nhcủa chương tr nh giao dịch là một vấn đề then chốt c ý nghĩa hết sức quan trọng.
Chính v l do đ trong luận văn thực hiện ở đ y một nghiên cứu s dụng phương ph p ph n t ch tĩnh để giải quyết bài toán tính cận trên bộ nhớ log của chương trình có giao dịch sẽ được trình bày, dựa trên bài báo đ được các tác giả công bố trong [1].
Mục tiêu nghiên cứu
Luận văn được thực hiện dựa trên nghiên cứu trong bài báo [1]. Do vậy để có thể hiểu được giải pháp các tác giả đ đề xuất trong [1], trong luận văn này tập trung nghiên cứu các lý thuyết về hệ thống kiểu; Các khái niệm cơ bản c ng như t nh chất của giao dịch; Nghiên cứu cú pháp và ngữ nghĩa của ngôn ngữ TM (Transactional Memory) – Một ngôn ngữ để viết các chương tr nh giao dịch. Từ việc nắm được giải pháp xây dựng hệ thống kiểu đề cập trong bài báo, một công cụ sẽ được cài đặt dựa trên ngôn ngữ C#.
Phương pháp nghiên cứu
Để thực hiện được mục tiêu đ đề ra trong luận văn c c phương ph p nghiên cứu sau đ y đ được kết hợp:
- Phương ph p nghiên cứu lý thuyết: bao gồm phân tích, tổng hợp các tài liệu, bài báo có liên quan về lý thuyết hệ thống kiểu đặc biệt là hệ thống kiểu cho c c chương trình TM, tài liệu về các thuật toán dựa trên hệ thống kiểu
- Phương ph p thực nghiệm: Cài đặt thuật to n đ đề xuất, ch y th để kiểm tra t nh đ ng đắn của chương tr nh.
Cấu trúc của luận văn
Luận văn được trình bày trong các phần, với nội dung chính của mỗi phần như sau:
Mở đầu: Nêu ra tính cấp thiết của đề tài, nêu ra các mục tiêu cần nghiên cứu, các phương ph p được s dụng khi nghiên cứu và cấu trúc các phần của luận văn.
Chương 1: Giới thiệu bài toán
Trình bày nội dung cụ thể của bài toán tính cận trên bộ nhớ log của chương tr nh có s dụng giao dịch, các vấn đề cần giải quyết trong bài to n này và hướng tiếp cận để giải quyết bài toán. Trong phần này, c c điểm cải tiến của phương ph p giải quyết bài toán ở đ y so với c c phương ph p trước kia c ng được nêu ra. Ví dụ được trình bày trong mục 1.3 sẽ minh họa rõ ràng cho bài to n và hướng tiếp cận đ đưa ra.
Chương 2: Một số kiến thức cơ sở
Trình bày các lý thuyết cơ bản được s dụng làm cơ sở để giải quyết bài toán, bao gồm: Lý thuyết về hệ thống kiểu như kh i niệm, các thuộc tính hay ứng dụng của hệ thống kiểu trong thực tế; Lý thuyết về giao dịch, bộ nhớ giao dịch phần mềm gồm các khái niệm, tính chất, ứng dụng
Chương 3: Ngôn ngữ giao dịch
Giới thiệu ngôn ngữ giao dịch TM (Transactional memory)- Một ngôn ngữ được d ng để viết c c chương tr nh giao dịch. Trong chương này cú pháp và ngữ nghĩa của ngôn ngữ TM sẽ được trình bày cụ thể.
Chương 4: Hệ thống kiểu cho chương trình giao dịch
Nghiên cứu hệ thống kiểu để giải quyết bài toán tính cận trên bộ nhớ log cho chương tr nh c giao dịch đ được trình bày trong bài báo [1]. Lý thuyết hệ thống kiểu được phát triển ở đ y bao gồm các kiểu và các quy tắc kiểu.
Chương 5: Xây dựng công cụ và thực nghiệm
Cài đặt các thuật toán kiểu dựa trên hệ thống kiểu đ được trình bày ở chương 4. Từ các thuật to n đ xây dựng công cụ để giải quyết bài toán tính cận trên bộ nhớ log và thực nghiệm để kiểm tra t nh đ ng đắn của công cụ.
Kết luận:
Đ nh gi c c kết quả đ đ t được, nêu ra tồn t i và hướng phát triển.

MỤC LỤC
LỜI CẢM ƠN .2
DANH MỤC CÁC KÝ HIỆU, THUẬT NGỮ, CHỮ VIẾT TẮT .5
DANH MỤC CÁC BẢNG .7
DANH MỤC CÁC HÌNH VẼ 7
MỞ ĐẦU 8
Tính cấp thiết của đề tài 8
Mục tiêu nghiên cứu .8
Phương ph p nghiên cứu 9
Cấu trúc của luận văn .9
CHƯƠNG 1. GIỚI THIỆU BÀI TOÁN .10
1.1. Giới thiệu .10
1.2. Hướng tiếp cận .11
1.3. Ví dụ minh họa 11
CHƯƠNG 2. MỘT SỐ KIẾN THỨC CƠ SỞ 14
2.1. Hệ thống kiểu .14
2.1.1. Giới thiệu về hệ thống kiểu .14
2.1.2. Các thuộc tính của hệ thống kiểu 16
2.1.3. Các ứng dụng của hệ thống kiểu .16
2.2. Giao dịch và bộ nhớ giao dịch phần mềm ( Software Transactional
Memory- STM) .18
2.2.1. Giao dịch (Transaction) 18
2.2.2. Bộ nhớ giao dịch phần mềm (Software Transactional Memory- STM)
.19
CHƯƠNG 3. NGÔN NGỮ GIAO DỊCH .21
3.1. Cú pháp của TM [1] .21
3.2. Các ngữ nghĩa động .21
3.2.1. Ngữ nghĩa cục bộ 21
3.2.2. Ngữ nghĩa toàn cục .22
4
CHƯƠNG 4. HỆ THỐNG KIỂU CHO CHƯƠNG TRÌNH GIAO DỊCH 24
4.1. Các kiểu .24
4.2. Các quy tắc kiểu .27
CHƯƠNG 5. XÂY DỰNG CÔNG CỤ VÀ THỰC NGHIỆM 30
5.1. Giới thiệu ngôn ngữ lập trình/ nền tảng .30
5.2. Xây dựng công cụ và thực nghiệm 30
5.2.1. Thuật toán rút gọn (chính tắc hóa) một chuỗi 31
5.2.2. Thuật toán Cộng (Joint) 33
5.2.3. Thuật toán gộp (Merge) 34
5.2.4. Thuật toán JoinCommit 37
5.2.5. Thuật toán tính cận trên tài nguyên của chương tr nh giao dịch 40
KẾT LUẬN .50
TÀI LIỆU THAM KHẢO 51