1. Họ và tên: Nguyễn Ngọc Khải                                     2. Giới tính: Nam

3. Ngày sinh: 27/10/1980                                                4. Nơi sinh: Thái Bình

5. Quyết định công nhận nghiên cứu sinh số: 1006/QĐ-CTSV ngày 07 tháng 12 năm 2015 của Hiệu trưởng Trường Đại học Công nghệ - Đại học Quốc Gia Hà Nội.

6. Các thay đổi trong quá trình đào tạo:

Đổi tên đề tài luận án theo Quyết định số 573/QĐ-ĐT ngày 22/6/2018 của Hiệu trưởng trường Đại học Công nghệ - Đại học Quốc Gia Hà Nội.

Tên đề tài cũ: Ước lượng tài nguyên sử dụng của các hệ thống phần mềm.

Tên đề tài mớ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.

7. Tên đề tài luận án: 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.

8. Chuyên ngành: Kỹ thuật phần mềm                            9. Mã số: 9480103.01

10. Cán bộ hướng dẫn khoa học: PGS.TS Trương Anh Hoàng

11. Tóm tắt các kết quả mới của luận án:

Những kết quả 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 của các chương trình STM (Software Transactional Memory) và một công cụ suy diễn kiểu cho chương trình:

Hệ thống kiểu thứ nhất bao gồm các quy tắc kiểu đơ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, 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 (hệ thống kiểu tích hợp) có khả năng định kiểu linh hoạt. 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 cả chương trình. 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.

Cuối cùng, dựa trên các quy tắc kiểu của hệ thống kiểu thứ nhất, chúng tôi đã cài đặt một công cụ suy diễn kiểu để định kiểu cho chương trình. Công cụ này được cài đặt bằng phương pháp lập trình hàm và ngôn ngữ lập trình F#, và nó đã vượt qua một số ca kiểm thử do chúng tôi đề xuất.

Ngoài những đóng góp chính ở trên, luận án cũng đã đưa ra một số cải tiến cho cơ chế STM để chúng sử dụng tài nguyên bộ nhớ hiệu quả hơn.

12. Khả năng ứng dụng trong thực tiễn:

Kết quả của luận án đã đóng góp những quy tắc kiểu mới cho cộng đồng nghiên cứu lý thuyết kiểu và phương pháp hình thức. Hệ thống kiểu này có thể được sử dụng làm nền tảng để phát triển các hệ thống kiểu cho những mục đích ước lượng các tài nguyên khác như lượng gas yêu cầu bởi các hợp đồng thông minh trong Ethereum, tài nguyên CPU, băng thông mạng.

Đối với công cụ suy diễn kiểu, khi nó được hoàn thiện, nó có thể được tích hợp vào các trình biên dịch hoặc các trình soạn thảo để cung cấp thông tin cho người lập trình về lượng tài nguyên tối đa cần sử dụng bởi chương trình STM.

Nghiên cứu này thiên về lý thuyết và nền tảng toán học cho các nghiên cứu trong tương lai. Việc cài đặt mới chỉ dừng lại ở việc cài đặt công cụ suy diễn kiểu. Để có thể ứng dụng trong các chương trình thực tế, chúng tôi cần thêm thời gian và nguồn lực.

13. Những hướng nghiên cứu tiếp theo:

Để có thể ứng dụng những kết quả của luận án, chúng tôi sẽ tiếp tục nghiên cứu cải tiến hệ thống kiểu và ngôn ngữ đã đề xuất theo hướng sau:

Đối với hệ thống kiểu: cải tiến các quy tắc kiểu để có thể định kiểu cho vòng lặp tổng quát và biên tài nguyên tìm được sắc hơn; tiếp tục hoàn thiện công cụ suy diễn kiểu để tích hợp vào các trình biên dịch, trình soạn thảo của ngôn ngữ lập trình để trợ giúp người lập trình.

Đối với ngôn ngữ: Nghiên cứu các công cụ để cài đặt thành ngôn ngữ thực tế; nghiên cứu các ngôn ngữ trong thực tế để xây dựng công cụ chuyển đổi giữa các ngôn ngữ thực tế và ngôn ngữ được đề xuất, nhằm áp dụng kết quả của luận án vào các ngôn ngữ thực tế.

14. Các công trình đã công bố có liên quan đến luận án:

[1] Ngoc-Khai Nguyen, Anh-Hoang Truong, and Duc-Hanh Dang. Finding transaction memory bound of STM programs. (Submitted to International Journal of Software Engineering and Knowledge Engineering Journal (IJSEKE), 2021).

[2] Ngoc-Khai Nguyen, Anh-Hoang Truong, and Duc-Hanh Dang. Estimate the memory bounds required by shared variables in software transactional memory programs. (Accepted by VNU Journal of Science: Computer Science and Communication Engineering, 2021).

[3] Nguyễn Ngọc Khải, Trương Anh Hoàng. Hệ thống kiểu để suy ra bộ nhớ log của chương trình giao dịch từ biến dùng chung. Tạp chí Khoa học và Kỹ thuật, Học viện Kỹ thuật quân sự, pp. 18-33, 2018.

[4] Ngoc-Khai Nguyen, and Anh-Hoang Truong. A Compositional Type Systems for Finding Log Memory Bounds of Transactional Programs. Proceedings of the Eighth International Symposium on Information and Communication Technology, pp. 409-416, ACM, 2017.

[5] Anh-Hoang Truong, Ngoc-Khai Nguyen, Dang Van Hung and Duc-Hanh Dang. Calculating statically maximum log memory used by multi-threaded transactional programs. Theoretical Aspects of Computing, pp.82-99, Springer, 2016.

[6] Trương Anh Hoàng, Nguyễn Ngọc Khải. 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. Tạp chí Khoa học - Đại học Sư phạm Hà Nội, pp. 80-93, 2015.