Luận án Tiến sĩ: Hệ thống kiểu ước lượng tĩnh tài nguyên chương trình giao dịch

ĐẠI HỌC 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 - ĐẠI HỌC 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. TRƯƠNG ANH HOÀNG Hà Nội - 2 Mục lục Trang Chương 1. Mục tiêu, đối tượng và phạm vi nghiên cứu. Mục tiêu nghiên cứu.

Đối tượng và phạm vi nghiên cứu. Những đóng góp chính, ý nghĩa khoa học và thực tiễn. Bố cục của luận án. KIẾN THỨC NỀN TẢNG VÀ NGHIÊN CỨU LIÊN QUAN.

Điều khiển tương tranh dựa trên khóa. Khái niệm khóa. Kỹ thuật khóa đơn giản. Kỹ thuật khóa đọc, ghi.

Kỹ thuật Semaphore. Một số vấn đề trong kỹ thuật khóa. Cơ chế bộ nhớ giao dịch phần mềm. Khái niệm và tính chất của giao dịch.

Đặc điểm của chương trình STM. Hệ thống kiểu. Khái niệm hệ thống kiểu. Một số tính chất cơ bản của hệ thống kiểu.

Ứng dụng và ý nghĩa của hệ thống kiểu. Hệ thống kiểu trong hình thức hóa ngôn ngữ. Nghiên cứu liên quan. Tài nguyên tiêu thụ trong chương trình tuần tự.

Tài nguyên tiêu thụ trong chương trình tương tranh. Tài nguyên tiêu thụ trong chương trình STM. 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. Tổng kết chương.

ƯỚC LƯỢNG BIÊN TÀI NGUYÊN CHƯƠNG TRÌNH CỦA NGÔN NGỮ TỐI GIẢN. Xác định số giao dịch tối đa. Ví dụ minh họa. Ngôn ngữ giao dịch tối giản.

Hệ thống kiểu tính số giao dịch tối đa. Quy tắc kiểu. Định kiểu chương trình ví dụ và thảo luận tính sắc của biên. Tính đúng của hệ thống kiểu.

Xác định biên tài nguyên tiêu thụ của chương trình. Ví dụ minh họa. Ngôn ngữ giao dịch tối giản cải tiến. Hệ thống kiểu tìm biên tài nguyên tiêu thụ của chương trình.

Quy tắc kiểu. Định kiểu cho chương trình ví dụ. Tính đúng của hệ thống kiểu. Tổng kết chương.

TÍNH BỘ NHỚ TỐI ĐA CHO CHƯƠNG TRÌNH CỦA NGÔN NGỮ MỆNH LỆNH. Ví dụ minh họa. Ngôn ngữ giao dịch với cấu trúc mệnh lệnh. Hệ thống kiểu tìm biên bộ nhớ cho các biến dùng chung.

Quy tắc kiểu. Định kiểu cho chương trình ví dụ. Công cụ suy diễn kiểu. Định nghĩa kiểu dữ liệu.

Hàm chính. Hàm hợp hai chuỗi. Hàm đồng kết thúc. Hàm chuyển dạng.

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. Quy tắc định kiểu. Đặc điểm của hệ thống kiểu. Định kiểu chương trình ví dụ và thảo luận tính sắc của biên.

Tổng kết chương. 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. Ví dụ minh họa. Phân tích hành vi của chương trình.

Phân tích bộ nhớ sử dụng bởi chương trình. Ngôn ngữ giao dịch với cấu trúc hướng đối tượng. Hệ thống kiểu tích hợp tìm biên bộ nhớ giao dịch. Quy tắc kiểu.

Định kiểu cho chương trình ví dụ. Tổng kết chương. Những kết quả đạt được. 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.2 Hệ thống kiểu liên kết với quá trình biên dịch.1 Mô tả hành vi của chương trình trong ví dụ.2 Đồng kết thúc các luồng.3 Mô tả hành vi của chương trình ví dụ 3.1 Mô tả hành vi hoạt động của ví dụ 4.2 Các giao dịch lồng nhau.3 Đồng kết thúc các luồng song song (trường hợp 1).4 Đồng kết thúc các luồng song song (trường hợp 2).5 Cây suy diễn kiểu cho đoạn chương trình e10 29 trong Đoạn mã 4.6 Hành vi của Đoạn chương trình trong Đoạn mã 4.7 Cây suy diễn kiểu của chương trình trong Đoạn mã 4.1 Mô phỏng hành vi của chương trình trong đoạn mã ví dụ 5.2 Giao dịch lồng nhau .3 Các hành phần tuần tự.4 Các luồng song song.5 Hợp hai luồng song song.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 .2 Ngữ nghĩa cục bộ của ngôn ngữ STM tối giản .3 Ngữ nghĩa giao dịch và luồng của ngôn ngữ STM tối giản .4 Quy tắc định kiểu cho chương trình STM tối giản .5 Cú pháp của ngôn ngữ giao dịch tối giản cải tiến .6 Ngữ nghĩa của ngôn ngữ giao dịch tối giản cải tiến .7 Quy tắc định kiểu chương trình STM tối giản cải tiến .1 Cú pháp của ngôn ngữ giao dịch cấu trúc mệnh lệnh .2 Ngữ nghĩa của ngôn ngữ giao dịch cấu trúc mệnh lệnh .3 Quy tắc kiểu .4 Quy tắc kiểu của hệ thống kiểu tích hợp .1 Cú pháp của ngôn ngữ STM hướng đối tượng .2 Ngữ nghĩa của ngôn ngữ STM hướng đối tượng .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.

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