Tài liệu Phương pháp dựa trên hệ thống kiểu để tính cận trên tài nguyên của các chương trình featherweight java có giao tác

3 MỤC LỤC LỜI CAM ĐOAN ..........................................................................................................................................1 LỜI CẢM ƠN ................................................................................................................................................2 MỤC LỤC ......................................................................................................................................................3 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 PHẦN MỞ ĐẦU ............................................................................................................................................8 Tính cấp thiết của đề tài .............................................................................................................................8 Mục tiêu của luận văn ................................................................................................................................9 Công cụ phần mềm.....................................................................................................................................9 Phƣơng pháp nghiên cƣ́u ............................................................................................................................9 Bố cục của luận văn ...................................................................................................................................9 CHƢƠNG 1. MỘT SỐ KIẾN THỨC CƠ SỞ .............................................................................................10 1.1. Các lý thuyết nền tảng về hệ thống kiểu ...........................................................................................10 1.1.1. Khái niệm hệ thống kiểu ............................................................................................................10 1.1.2. Vai trò của hệ thống kiểu ...........................................................................................................11 1.1.3. Các thuộc tính cơ bản của hệ thống kiểu ....................................................................................13 1.1.4. Các ứng dụng và ý nghĩa kinh tế của hệ thống kiểu ...................................................................14 1.1.5. Hệ thống kiểu trong việc chính thức hóa ngôn ngữ kiểu ............................................................16 1.2. Bộ nhớ giao tác phần mềm ................................................................................................................18 1.2.1. Khái niệm và các thuộc tính cơ bản của giao tác .......................................................................18 1.2.2. Bộ nhớ giao tác phần mềm .........................................................................................................19 CHƢƠNG 2. FEATHERWEIGHT JAVA CÓ GIAO TÁC ........................................................................23 2.1. Cú pháp .............................................................................................................................................23 2.2. Các ngữ nghĩa....................................................................................................................................24 2.2.1. Ngữ nghĩa cục bộ .......................................................................................................................24 2.2.2. Ngữ nghĩa toàn cục ....................................................................................................................26 CHƢƠNG 3. HỆ THỐNG KIỂU CHO TFJ ................................................................................................30 3.1. Các kiểu .............................................................................................................................................30 3.2. Các qui tắc kiểu .................................................................................................................................38 3.2.1. Qui tắc cục bộ .............................................................................................................................38 3.2.2. Qui tắc toàn cục ..........................................................................................................................41 CHƢƠNG 4. THUẬT TOÁN KIỂU VÀ CÔNG CỤ ..................................................................................44 4.1. Xây dựng bộ cú pháp cho TFJ với ANTLR ......................................................................................44 4.1.1. Cơ sở lý thuyết về cú pháp đƣợc hỗ trợ bởi ANTLR .................................................................44 4.1.2. Bộ đặc tả cú pháp cho TFJ với ANTLR V3 ...............................................................................45 4 4.2. Xây dựng thuật toán tính kiểu ...........................................................................................................48 4.2.1. Rút gọn một chuỗi số có dấu bất kỳ về chuỗi số chính tắc .......................................................48 4.2.2. Mô tả phép toán cộng ⊕ của 2 chuỗi số có dấu chính tắc .........................................................49 4.2.3. Mô tả phép toán gộp ⊗ của 2 chuỗi số có dấu chính tắc ...........................................................50 4.2.4. Mô tả phép toán điều kiện , phép toán chọn ⊙, của 2 chuỗi số có dấu chính tắc ......................50 4.2.5. Tính toán giá trị mức giới hạn trên tổng chi phí tài nguyên cho một chƣơng trình TFJ ............51 CHƢƠNG 5. THỰC NGHIỆM ...................................................................................................................58 KẾT LUẬN ..................................................................................................................................................63 TÀI LIỆU THAM KHẢO ............................................................................................................................64 PHỤ LỤC .....................................................................................................................................................65 PHỤ LỤC 1. CÁC CÔNG CỤ HỖ TRỢ CÀI ĐẶT THỰC NGHIỆM ...................................................65 PHỤ LỤC 2. BẢNG MÔ TẢ CHI TIẾT ĐẶC TẢ CÚ PHÁP TFJ TRÊN ANTLR V3 .........................69 PHỤ LỤC 3. BẢNG MÔ TẢ CÁC PHƢƠNG THỨC TRONG CHƢƠNG TRÌNH..............................85 5 DANH MỤC CÁC KÝ HIỆU , THUẬT NGỮ, CHỮ VIẾT TẮT STT CHỮ VIẾT TẮT, THUẬT NGỮ, KÝ HIỆU GIẢI NGHĨA CHỮ VIẾT TẮT 1 2 3 FJ –Featherweigh Java STM - Software Transactional Memory TFJ – Transactional Featherweight Java Một ngôn ngữ Java tối giản để nghiên cứu các tính chất của Java. Bộ nhớ giao tác phần mềm, một giải pháp viết các chƣơng trình tƣơng tranh, thay cho cơ chế đồng bộ dựa trên khóa. Là một ngôn ngữ mở rộng của FJ tích hợp mô hình bộ nhớ giao tác phần mềm. THUẬT NGỮ 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 Type System Transaction Thread Excution errors Syntactic mechanism Type checker Well-behaved Well-formed Ill-behaved Execution error Well-typed Ill-typed ADT-Abstract Data Type Efficiency Compositionality Guarantee Static phase 17 18 Dynamic phase Hệ thống kiểu Giao tác Luồng Lỗi thực thi Cơ chế cú pháp Bộ kiểm tra kiểu Tính chất hành xử đúng của chƣơng trình. Tính chất thiết lập đúng của chƣơng trình. Tính chất hành xử yếu của chƣơng trình. Lỗi thực thi Một chƣơng trình khi đƣợc thông qua bởi bộ kiểm tra kiểu đƣợc gọi là kiểu tốt. Một chƣơ ng trì nh không đƣợc thông qua bởi bộ kiểm tra kiểu đƣợc gọi là kiểu yếu. Kiểu dữ liệu trừu tƣợng Hiệu suất chƣơng trình Tính thành phần Tính đảm bảo Pha tĩnh, đặc tả bởi tập các qui tắc đánh giá kiểu một biểu thƣ́c nói riêng và một chƣơng trình nói chung có là well-formed. Pha động, là một mô tả chƣơng trình đƣợc thực hiện nhƣ thế nào. 6 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 Atomicity Consistency Isolation Durability Onacid Commit Lock-based synchronization Nested transactions Multi-threaded Spawn Joint commits Local semantics Global semantics Local enviroments Global enviroments Syntax Term Tính nguyên tử Tính nhất quán Tính độc lập Tính bền vững Trạng thái mở một giao tác Trạng thái kết thúc một giao tác Đồng bộ hóa dựa trên khóa Các giao tác lồng Đa luồng Sinh luồng Các commit của các luồng song song đồng thời thực hiện kết thúc một giao tác chung. Ngữ nghĩa cục bộ Ngữ nghĩa toàn cục Môi trƣờng cục bộ Môi trƣờng toàn cục Cú pháp Các thành phần trong biểu thức cú pháp. KÝ HIỆU + m 1 - m 2 # 3 m ¬ m 4 Mô tả thành phần + trong hệ thống kiểu dựa trên chuỗi số có dấu, m thao tác onacid liên tiếp. Mô tả thành phần – trong hệ thống kiểu dựa trên chuỗi số có dấu, m thao tác commit liên tiếp. Mô tả thành phần # trong hệ thống kiểu dựa trên chuỗi số có dấu, m các giao tác lồng nhau. Mô tả thành phần ¬ thể hiện số lƣợng joint commit trong hệ thống kiểu dựa trên chuỗi số có dấu. 7 DANH MỤC CÁC BẢNG Bảng 2.1 Cú pháp TFJ [17] ................................................................................................ 23 Bảng 2.2 Ngữ nghĩa cục bộ [17] ........................................................................................ 25 Bảng 2.3 Ngữ nghĩa toàn cục [17]...................................................................................... 27 Bảng 3.1 Hệ thống kiểu mức cục bộ[17] ............................................................................ 40 Bảng 3.2 Hệ thống kiểu mức toàn cục[17] ......................................................................... 41 Bảng 4.1 Tổng quát hóa các rule của EBNF [18] .............................................................. 44 Bảng 4.2 Bảng kết quả kiểm thử phép toán chính tắc chuỗi số có dấu .............................. 49 Bảng 4.3 Bảng kết quả kiểm thử phép toán cộng 2 chuỗi số có dấu chính tắc .................. 50 Bảng 4.4 Bảng kết quả kiểm thử phép toán gộp 2 chuỗi số có dấu chính tắc .................... 50 Bảng 4.5 Bảng kết quả kiểm thử phép toán chọn 2 chuỗi số có dấu chính tắc .................. 51 Bảng PL-0 1 Chú giải chi tiết các rule trong cú pháp của ngôn ngữ TFJ .......................... 69 Bảng PL-0 2 Mô tả các phƣơng thức dùng để tính toán giới hạn trên chi phí tài nguyên . 85 DANH MỤC CÁC HÌNH VẼ Hình 1.1 Hệ thống kiểu trong trình biên dịch[10] .............................................................. 17 Hình 1.2 Sơ đồ các trạng thái của giao tác ......................................................................... 18 Hình 1.3 Ví dụ giả mã cho mô hình giao tác lồng và đa luồng .......................................... 20 Hình 1.4 Ví dụ mô hình giao tác lồng, đa luồng và joint ................................................... 20 Hình 1.5 Ví dụ mô hình giao tác thể hiện tính phụ thuộc các luồng song song ................. 21 Hình 3.1 Mô tả hai thành phần # liền kề ............................................................................ 32 Hình 3.2 Minh họa ý nghĩa thành phần ¬ ........................................................................... 34 Hình 3.3 Mô hình mô tả spawn ở thời điểm cuối của biểu thức ........................................ 40 Hình 4.1 Mô tả các bƣớc lấy đƣợc chuỗi StringTFJPrimitive ........................................... 47 Hình 4.2 Mô tả các giai đoạn để tính giá trị giới hạn trên tài nguyên ................................ 51 Hình 4.3 Mô hình chƣơng trình TFJ cho Ví dụ 4.3 ............................................................ 53 Hình 4.4 Minh họa ví dụ các giai đoạn để tính giới hạn trên tổng chi phí tài nguyên ....... 53 Hình 5.1 Mô hình giao tác Thực nghiệm 1 ........................................................................ 58 Hình 5.2 Chạy mã Thực nghiệm 1 trên công cụ................................................................. 59 Hình 5.3 Mô hình giao tác cho Thực nghiệm 2 .................................................................. 61 Hình 5.4 Chạy mã Thực nghiệm 2 trên công cụ tính kiểu tự động .................................... 62 Hình PL-0 1 Tạo mới một Project ...................................................................................... 66 Hình PL-0 2 Tạo một tệp ngữ pháp trong ANTLR ............................................................ 68 8 PHẦN MỞ ĐẦU Tính cấp thiết của đề tài Gần đây các máy tính và điện thoại đƣợc trang bị nhiều bộ xử lý hay các bộ xử lý có nhiều nhân (core). Để khai thác hết khả năng chạy song song của các bộ xử lý này cần có các tiến trình hoặc luồng (process, thread) có khả năng tính toán song song. Các ngôn ngữ lập trình truyền thống sử dụng cơ chế khóa và đồng bộ (lock, synchronization) để các tiến trình cùng hoạt động và truy cập đến các biến dùng chung. Tuy nhiên, phƣơng pháp này dễ gây ra các khóa chết (deadlock) hoặc các lỗi tiềm ẩn rất khó phát hiện và sửa chữa. Software Transactional Memory (STM- bộ nhớ giao tác phần mềm) [15], là một giải pháp mới để viết các chƣơng trình song song sử dụng cơ chế giao tác (transaction) của các hệ quản trị cơ sở dữ liệu thay cho cơ chế đồng bộ dựa trên khóa đối với việc chia sẻ bộ nhớ đồng thời. STM xử lý với bộ nhớ thông qua các giao tác, mỗi giao tác cho phép tự do đọc và ghi để chia sẻ các biến khi đƣợc khởi động (onacid) và một log đƣợc sử dụng để ghi các hoạt động này cho tới thời điểm kết thúc (commit). Tuy nhiên, một vấn đề phát sinh mô hình STM này sử dụng thêm khá nhiều tài nguyên (bộ nhớ, xử lý), do các log là các bản sao của thông tin, biến, khi tính toán để thực hiện commit hoặc rollback khi tính toán bị thất bại xong. Hệ thống kiểu là một phƣơng pháp phân tích tĩnh dựa trên các qui tắc kiểu đã đặt ra để đƣa ra các khẳng định chƣơng trình có thành lập đúng hoặc an toàn hay không, từ đó, nó hạn chế các lỗi tiềm tàng có thể xảy ra. Hệ thống kiểu cũng có thể ƣớc lƣợng an toàn thông tin về tài nguyên sử dụng của chƣơng trình mà không cần thực thi nó[5]. Việc này có ý nghĩa thực tiễn vì với một chƣơng trình đã cho ta biết đƣợc trong trƣờng hợp xấu nhất nó có thể cần bao nhiêu bộ nhớ. Một số hệ thống kiểu trƣớc kia khi giải quyết vấn đề tính toán tài nguyên tĩnh cho một chƣơng trình có giao tác thông qua thể hiện cây phân cấp [13] và tổng tài nguyên đƣợc tính theo nguyên tắc cộng dồn, khi đó giới hạn trên tổng tài nguyên đƣa ra là con số khá lớn. Luận văn nghiên cứu một hệ thống kiểu mới [17] sử dụng các chƣơng trình Featherweight Java có giao tác (Transactional Featherweight Java, gọi tắt là TFJ). Hệ thống kiểu ƣớc lƣợng tài nguyên tiêu tốn chính xác hơn so với các nghiên cứu trƣớc đó [6, 13]. Những vấn đề nêu trên là cơ sở khoa học và thực tiễn để tôi thực hiện đề tài “Phương pháp dựa trên hệ thống kiểu để tính cận trên tài nguyên của các chương trình Featherweight Java có giao tác”. 9 Mục tiêu của luận văn Trên cơ sở nghiên cứu lý thuyết về hệ thống kiểu , để xác định tài nguyên của các chƣơng trình Featherweight Java có giao tác (TFJ) [17], đề tài đƣa ra phƣơng pháp tính tài nguyên của các chƣơng trình TFJ và cài đặt một công cụ phần mềm có khả năng tính tài nguyên sử dụng của các chƣơng trình TFJ đó. Công cụ phần mềm Sử dụng thƣ viện và công cụ hỗ trợ ANTLR để phân tích mã nguồn của chƣơng trình TFJ. Các công cụ lập trình trên nền .NET và ngôn ngữ C # để cài đặt thuật toán chƣơng trình. Phƣơng pháp nghiên cƣ́u Để đề tài đạt đƣợc kết quả nhƣ mục tiêu đặt ra, trong luận văn tôi đã đề xuất và áp dụng các phƣơng pháp nghiên cứu nhƣ sau: - Nghiên cứu tài liệu: Nghiên cứu hệ thống kiểu nói chung và tập trung vào hệ thống kiểu cho các chƣơng trình TFJ nhƣ đã nêu trong [17]. Đây là mảng kiến thức mới, không đƣợc học ở trƣờng và đòi hỏi nhiều kiến thức nền tảng liên quan. Đồng thời ở đây tôi cũng phải nghiên cứu các thuật toán dựa trên hệ thống kiểu đã đề xuất để có thể tính tài nguyên cho một chƣơng trình TFJ. - Cài đặt, thực nghiệm: Nghiên cứu các công cụ phân tích chƣơng trình và thƣ viện hỗ trợ (ANTLR) để sử dụng phân tích một chƣơng trình đầu vào. Từ đó cài đặt thuật toán đề xuất, đồng thời chạy thử, kiểm tra tính đúng đắn của công cụ. Bố cục của luận văn Trong luận văn sẽ đƣợc thƣ̣c hiện bởi các phần cơ bản: - Phần mở đầu: Đƣa ra tính cấp thiết của đề tài, công cụ phần mềm sử dụng, phƣơng pháp nghiên cứu và bố cục của luận văn. - Chƣơng 1: Nghiên cƣ́u một số các kiến thức cơ sở về hệ thống kiểu và bộ nhớ giao tác phần mềm. - Chƣơng 2: Nghiên cứu về cú pháp và các ngữ nghĩa tổng quát của chƣơng trình Featherweight Java có giao tác. - Chƣơng 3: Nghiên cứu hệ thống kiểu cho các chƣơng trình TFJ: Đị nh nghĩa, tập các qui tắc kiểu dựa trên chuỗi số có dấu. - Chƣơng 4: Xây dựng thuật toán tính kiểu và công cụ: Các phép toán tính toán kiểu, tính giới hạn trên tổng chi phí tài nguyên cho các chƣơng trình TFJ. - Chƣơng 5: Thực nghiệm: Kiểm tra chƣơng trình tính kiểu xây dựng ở Chƣơng 4 là đúng thông qua các ví dụ thực nghiệm với các chƣơng trình TFJ. - Kết luận: Tổng hợp các kết quả đạt đƣợc, tồn tại và hƣớng mở rộng của đề tài. 10 CHƢƠNG 1. MỘT SỐ KIẾN THỨC CƠ SỞ 1.1. Các lý thuyết nền tảng về hệ thống kiểu 1.1.1. Khái niệm hệ thống kiểu Hệ thống kiểu (type system) trong toán học đã xuất hiện từ đầu thế kỷ 19. Đến nay hệ thống kiểu có sức ảnh hƣởng và có ý nghĩa to lớn [1]. Đã có rất nhiều quan điểm khác nhau về hệ thống kiểu: Một hệ thống kiểu là một phƣơng pháp kiểm soát cú pháp cho việc chứng minh sự vắng mặt của các hành vi nào đó của chƣơng trình bằng cách phân loại các thành phần theo kiểu cho các giá trị nó tính toán [1]. Luca Cardelli phát biểu rằng: Hệ thống kiểu là một phƣơng pháp chính thức ngăn chặn các lỗi thực thi trong quá trình chạy của chƣơng trình [3, 5]. Dƣới góc độ của ngƣời lập trình, một hệ thống kiểu là tập các chú thí ch kiểu và cơ chế kiểm tra trợ giúp cho ngƣời lập trình. Với ngƣời viết trì nh dị ch , một hệ thống kiểu là nguồn thông tin có thể đƣợc sƣ̉ dụng để tối ƣu mã máy sinh ra . Theo lý thuyết ngôn ngữ, một hệ thống kiểu là một bộ qui tắc để qui định cấu trúc và lập luận về ngôn ngƣ̃. Nói tóm lại hệ thống kiểu đóng vai trò quan trọng với các ngôn ngữ lập trình [8]. Ta có thể khái quát hóa khái niệm hệ thống kiểu nhƣ sau: Hệ thống kiểu là một cơ chế cú pháp (syntactic mechanism) ràng buộc cấu trúc của một chương trình bởi việc kết hợp các thông tin ngữ nghĩ a với các thành phần trong chương trình và giới hạn phạm vi của các thành phần đó. Theo đó đặc trƣng của ngôn ngữ đƣợc thiết kế trên hệ thống kiểu đòi hỏi mỗi biến trong chƣơng trì nh phải có miền giá trị cụ thể mà nó có thể tham chiếu , mỗi khai báo hàm cũng phải thao tác trên các kiểu đối số cụ thể và trả về giá trị của kiểu cụ thể. Thông tin này có thể đƣợc khai báo rõ ràng bằng cách sƣ̉ dụng các chú thí ch kiểu hoặc suy ra bởi bộ kiểm tra kiểu (type checker). Khi một chƣơng trì nh đƣợc biên dị ch , một bộ kiểm tra kiểu này đảm bảo rằng mỗi biến chỉ đƣợc gán đúng kiểu của giá trị và các hàm chỉ đƣợc gọi với các tham số đúng kiểu. Các ngôn ngữ hạn chế phạm vi của các biến đƣợc gọi là ngôn ngữ kiểu , nhƣ ML hoặc C. Ngƣợc lại, ta hiểu đó là ngôn ngữ phi kiểu, nhƣ LISP, Assembler. Một hệ thống kiểu là thành phần của một ngôn ngƣ̃ kiểu, có vai trò theo dõi các kiểu của các biến và các kiểu của tất cả các biểu thƣ́c trong chƣơng trì nh. Trong một ngôn ngữ có hệ thống kiểu mà giƣ̃ cho tất cả chƣơng trì nh chạy đƣợc trên ngôn ngƣ̃ lập trì nh cụ thể, chúng ta nói rằng ngôn ngữ là kiểu tốt (well typed). Nó chỉ ra rằng, một phân tí ch cẩn thận là cần thiết để tránh nhƣ̃ng tuyên bố sai cho các ngôn ngƣ̃ lập trì nh. Một hệ thống kiểu đƣợc sƣ̉ dụng để xác đị nh liệu chƣơng trì nh có đƣợc coi là well-behaved (hành xử đúng). Do vậy, các chƣơng trình đƣợc thực hiện theo một hệ thống 11 kiểu nên đƣợc xem xé t là các chƣơng trì nh thƣ̣c sƣ̣ của ngôn ngƣ̃ kiểu , các chƣơng trình khác nên đƣợc loại bỏ trƣớc khi chạy. Khi phát triển một cách đúng đắn , các hệ thống kiểu cung cấp các công cụ khái niệm để đánh giá một cách đầy đủ cá c khí a cạnh quan trọng của các đị nh nghĩ a ngôn ngƣ̃ . Mô tả ngôn ngƣ̃ chí nh thƣ́c thƣờng không xác đị nh cấu trúc của một ngôn ngƣ̃ đầy đủ chi tiết để cho phép thƣ̣c thi rõ ràng . Thƣờng xảy ra với các trì nh biên dị ch khác nhau cho cùng một ngôn ngữ cài đặt các hệ thống kiểu khác nhau . Hơn nƣ̃a, nhiều đị nh nghĩ a ngôn ngƣ̃ đã đƣợc tì m thấy là kiểu không đúng đắn , theo đó một chƣơng trì nh có thể sụp đổ mặc dù các đánh giá đƣợc chấp nhận bởi bộ k iểm tra kiểu . Lý tƣởng nhất , hệ thống kiểu chính thức nên là một phần định nghĩa tất cả các ngôn ngữ lập trình đƣợc định kiểu . Bằng cách này, các thuật toán kiểm tra kiểu có thể đƣợc đo đạc một cách rõ ràng dựa vào các thông số kỹ thuật chí nh xác nếu tất cả có thể và khả thi , ngôn ngƣ̃ có thể đƣợc thể hiện là kiểu đúng đắn. Một ngôn ngƣ̃ đƣợc đị nh kiểu bởi sƣ̣ tồn tại của hệ thống kiểu cho nó , có hay không các kiểu trong cú phá p chƣơng trì nh . Các ngôn ngữ kiểu đƣợc định kiểu rõ ràng nếu các kiểu là thành phần của cú pháp . Tuy vậy, ta cũng phải khẳng định rằng không có ngôn ngƣ̃ chí nh thống hoàn toàn đƣợc đị nh kiểu , các ngôn ngữ nhƣ ML và Haskell hỗ trợ viết các đoạn chƣơng trì nh lớn , nơi các thông tin kiểu đƣợc bỏ qua , các hệ thống kiểu của ngôn ngƣ̃ tƣ̣ động gán các kiểu cho các đoạn chƣơng trì nh nhƣ vậy . Do đó tùy từng bài toán mà có thể áp dụng một ngôn ngữ định kiểu hay ngôn ngữ không định kiểu để cài đặt. 1.1.2. Vai trò của hệ thống kiểu Hệ thống kiểu là cần thiết cho các ngôn ngữ lập trình. Thông thƣờng hệ thống kiểu trong các ngôn ngƣ̃ lập trì nh có 4 vai trò chí nh [8] thể hiện: a) Phát hiện lỗi Trong quá trình thực thi có thể xảy ra các loại lỗi khác nhau, có lỗi có tác động ngay lập tức đến kết quả của chƣơng trình hoặc có những lỗi trong đó kết quả có thể làm thay đổi dữ liệu mà không có tác động ngay lập tức. Ví dụ nhƣ: Ví dụ 1.1 Lỗi lệnh không hợp lệ khai báo biến trong C#. Trong khai báo từ biến của C#. int x; Lỗi này không hợp lệ vì trong C# không cho phép khai báo một biến mà không gán trị. Và lỗi này sẽ gây tác động dừng thực thi ngay lập tức. Ta có thể sửa cho đúng bằng cách gán trị cho nó nhƣ: int x=0; 12 Ví dụ 1.2 Lỗi không hợp lệ khai báo tham số không phù hợp trong C#. private static int sum(String x, String y) { int result = x+y; return result; } Lỗi này hoàn toàn không hợp lệ bởi lẽ biến result của chúng ta là biến kiểu int trong khi đó x,y là hai biến có kiểu String. Điều này trong ngôn ngữ C# không cho phép và lỗi này cũng dẫn đến dừng chƣơng trình ngay lập tức. Ta có thể sửa lại cho đúng thành: private static int sum(String x, String y) { int result = Int32.Parse(x)+ Int32.Parse(y); return result; } Tuy nhiên có nhiều dạng lỗi thƣ̣c thi mà kết quả thay đổi dƣ̃ liệu mà không có tác động ngay lập tƣ́c. Ví dụ nhƣ phƣơng thức tính giai thừa trong C# cho nhƣ sau: Ví dụ 1.3 Tính giai thừa của số nguyên n. private int fact(int n) { if(n>0) return n * fact(n – 1); return 1; } Đối với chƣơng trình trên thì trình biên dịch hoàn toàn không phát hiện ra lỗi nếu nhƣ chúng ta đƣa giá trị đầu vào hợp lý nhƣ n=2 hoặc n=5, … Tuy nhiên, nếu n=27 thì chƣơng trình sẽ thông báo lỗi vì quá phạm vi cho phép của kiểu int trong C# (32bit). Một trong các mục đích cơ bản của hệ thống kiểu là ngăn chặn sự xuất hiện của các lỗi thực thi (Ví dụ 1.1 và Ví dụ 1.2), lỗi mà có thể xảy ra trong thời gian chạy chƣơng trình. Bên cạnh đó, cũng có khi lỗi thực thi có thể là tiềm tàng, hệ thống kiểu không thể phát hiện ra nhƣ Ví dụ 1.3 . Do đó, độ chính xác của hệ thống kiểu phụ thuộc vào vấn đề khá tinh tế của những gì tạo ra một lỗi thực thi (execution error). Hệ thống kiểu theo dõi các kiểu của các đối số , chúng có thể phát hiện từng phần mã lệnh gán giá trị không hợp lệ . Hệ thống kiểu có thể phát hiện lỗi luồng dƣ̃ liệu logic trong chƣơng trì nh.Vì vậy, chúng có thể đả m bảo sƣ̣ vắng mặt của lớp nào đó của các lỗi lập trì nh tƣ̀ các chƣơng trì nh. Nhiều lỗi lập trì nh chung qui là sƣ̉ dụng dƣ̃ liệu sai ở các vị trí sai . Hệ thống kiểu phân chia vùng giá trị hợp lệ có thể xuất hiện trong ngƣ̃ cảnh của chƣơng trì nh và kiểm tra 13 cho phù hợp phân vùng này ở thời gian biên dị ch . Ngƣời lập trì nh có thể dƣ̣a trên nó để phát hiện lỗi chƣơng trình trƣớc khi chƣơng trình đƣợc thực hiện. b) Trừu tượng hóa Các kiểu đƣợc sƣ̉ dụng để trƣ̀u tƣợng các thành phần của một chƣơng trì nh . Nhiều nghiên cƣ́u đã đƣợc thƣ̣c hiện trên các kiểu dƣ̃ liệu trƣ̀u tƣợng (ADT-Abstract Data Type), cơ sở c ho đị nh nghĩ a các kiểu mới , đi cấu trúc bên trong của nó với phần còn lại của một chƣơng trình. Kiểu dƣ̃ liệu trƣ̀u tƣợng có thể có c ác giao diện cơ bản của nó , che dấu thông tin hạn chế sƣ̣ phụ thuộc các modul e của chƣơng trình, làm cho nó có thể thay đổi việc thƣ̣c hiện cơ bản tƣ̀ một ADT miễn là tí nh bất biến đƣợc bảo tồn . Các kiểu dữ liệu trƣ̀u tƣợng trong hệ thống kiểu đƣợc dùng cho các ngôn ngƣ̃ hƣớng đối tƣợng. Một hì nh thƣ́c trƣ̀u tƣợng khác đƣợc trì nh bày bởi hệ thống kiểu là tí nh đa h ình, cung cấp các đị nh nghĩ a với các đị nh danh giống nhau có thể đƣợc hợp thành một dƣ̣a trên các kiểu của các biểu thƣ́c con trong ngƣ̃ cảnh nơi nó đƣợc sƣ̉ dụng . Ví dụ , nhiều ngôn ngƣ̃ cung cấp tí nh đa hì nh đơn giản nhƣ cá c phép toán giống nhƣ phép cộng và phép nhân đƣợc đị nh nghĩ a cho cả số nguyên, số thập phân, con trỏ số thƣ̣c. c) Tài liệu Nhiều ngôn ngƣ̃ kiểu tĩ nh yêu cầu các lập trì nh viên nhập chú thích một số thành phần của chƣơng trì n h với kiểu thông tin . Ví dụ trong ngôn ngữ lập trình C , tất cả các biến phải khai báo kiểu của giá trị cho nó, mọi định nghĩa hàm tƣơng ứng phải đƣợc khai báo kiểu của các đối số và kiểu trả về. Việc chú thí ch là rất hƣ̃u í ch. d) Tăng hiệu quả Một chƣơng trì nh đƣợc thiết lập kiểu tốt (well-type) cung cấp một trì nh biên dị ch , với thông tin mà trì nh biên dị ch có thể sƣ̉ dụng mục đí ch cải thiện quá trì nh dị ch chƣơng trình. Ngay cả các biến có kiểu tĩ nh , trình biên dịch có thể quyết đị nh vị trí thể hiện các biến này nhƣ thế nào trong mã máy. Điều này đặc biệt hƣ̃u í ch khi một biến chỉ có thể giƣ̃ một giá trị kiểu cố đị nh. Ví dụ, hầu hết các kiến trúc máy tí nh hiện đại cung cấp các thanh ghi đặc biệt xƣ̉ lý các dấu phẩy động nhƣng chúng chỉ có thể đƣợc sƣ̉ dụng khi giá trị là có dấu phẩy động. Cho một thông tin kiểu, trình biên dịch có thể xác định một tham số từ một hàm luôn là một số có dấu phẩy động . Trình biên dịch có thể dịch hàm cũn g nhƣ nhận đối số dấu phẩy động trong một thanh ghi chƣ́ không phải trong bộ nhớ . Hệ thống kiểu không đảm bảo chƣơng trì nh sẽ hoạt động nhƣ thế nào. 1.1.3. Các thuộc tính cơ bản của hệ thống kiểu Hầu hết các hệ thống kiểu đều thể hiện các thuộc tính chung nhƣ sau [8]: a) Thuộc tí nh kiểu (types) 14 Mỗi một ngôn ngƣ̃ định kiểu có một tập các kiểu , nó là những thực thể cơ bản đại điện cho tí nh chất ngƣ̃ nghĩ a . Các ngôn ngữ cơ bản cung cấp một tập các kiểu nguyên thủy, nhƣ số nguyên , logic, hoặc các kiểu định nghĩa từ kiểu nguyên thủy nhƣ mảng số nguyên, danh sách. Trong trƣờng hợp đơn giản , tất cả các kiểu đƣợc biểu thị bởi một tên đặc biệt và duy nhất . Các ngôn ngữ phức tạp hơn cho phép lập trình viên khai báo giả kiểu, thay thế tên cho cùng một kiểu . Hầu hết các ngôn ngƣ̃ cũng cung cấp các cấu trúc , cho phép lập trì nh viên có thể đị nh nghĩ a kiểu tổng hợp tƣ̀ các kiểu khác. Cấu trúc của các tên kiểu thƣờng mã hóa một số thông tin ngƣ̃ nghĩ a về loại giá trị có thể có kiểu nhất đị nh. Ví dụ kiểu hàm AB mô tả một hàm lấy giá trị kiểu A và giá trị trả về kiểu B. b) Tính kết hợp (compositionality) Trong ngôn ngƣ̃ kiể u, mỗi biểu thƣ́c có một kiểu và kiểu đó là kiểu trả về tƣ̀ các biểu thƣ́c con của nó . Cho ví dụ, hãy xem xét biểu thức if a then b else c. Trong một ngôn ngƣ̃ các biểu thƣ́c này đƣợc xác đị nh đầy đủ 3 biểu thƣ́c con a, b,c. Đầu tiên a có kiểu logic và b, c phải cùng kiểu.Với nhƣ̃ng hạn chế này toàn bộ biểu thƣ́c có cùng kiểu với cả b và c. Qui tắc này cho biết biểu thƣ́c trả về hoặc là b hoặc là c. Mặc dù có kiểu biểu thƣ́c well-type đƣa ra mối quan hệ thành phần, việc gán các kiểu phụ thuộc vào ngƣ̃ cảnh. c) Tính bảo đảm (guarantee) Các hệ thống kiểu hiện đại cố gắng làm nhiều hơn so với các cơ chế lộn xộn hiện tại cho các ràng buộc giá trị mà các biến có thể nhận. Các nhà lý thuyết ngôn ngữ lập trình đã phát triển kỹ thuật ngƣ̃ nghĩ a thể hiện các liên hệ giữa ngôn ngữ lập trình và kiểu của nó. Đặc tả chính thức ngôn ngữ dƣ̣a trên các ngƣ̃ nghĩ a tĩ nh (đảm bảo chƣơng trì nh là thiết lập đúng cách hay không ) và ngữ nghĩa động (đảm bảo chƣơng trì nh hành xƣ̉ đúng hay không) của nó . Để liên hệ các ngƣ̃ nghĩ a động với ngƣ̃ nghĩ a tĩ nh , các nhà thiết kế ngôn ngƣ̃ chƣ́ng minh một tập các đị nh lý để thiết lập các thuộc tí nh độ ng của các chƣơng trình này, cái mà là well-type bởi các ngƣ̃ n ghĩa tĩnh. Ý tƣởng này đảm bảo chƣơng trình duy trì đồng bộ well-type nhƣ nó thƣ̣c thi và một chƣơng trì nh well-type sẽ không nằm ngoài phạm vi ngữ nghĩa động. 1.1.4. Các ứng dụng và ý nghĩa kinh tế của hệ thống kiểu Hệ thống kiểu đóng vai trò lớn trong phần mềm máy tính và bảo mật mạng : Kiểu tĩnh nằm ở nhân của các mô hình bảo mật , của Java và JINI là một ví dụ . Hệ thống kiể u đƣợc sƣ̉ dụng trong các trình biên dịch , xác minh các giao thức , cấu trúc thông tin trên web và thậm chí mô hì nh các ngôn ngƣ̃ tƣ̣ nhiên . Một số ứng dụng mà hệ thống kiểu thƣờng có mặt nhƣ: Trong lập trì nh hệ thống lớn (chứa hệ thống các module ), trong biên 15 dịch và tối ƣu hóa (các phân tích tĩnh, các ngôn ngữ kiểu trung gian), trong bảo mật, trong chƣ́ng minh các đị nh lý và trong cơ sở dƣ̃ liệu. Vấn đề về các ngôn ngƣ̃ lập trì nh nên có kiểu vẫn còn là một số tranh luận , có rất í t nghi ngờ rằng mã đƣợc viết bằng ngôn ngƣ̃ không đị nh kiểu có thể đƣợc duy trì chỉ với khó khăn rất lớn . Tƣ̀ quan điểm của bảo trì , thậm chí ngôn ngƣ̃ kiểm tra yếu không an toàn vƣợt trội so với các ngôn ngữ an toà n nhƣng không đị nh kiểu (ví dụ C so với LISP ). Dƣới đây là các lập luận đã đƣợc đƣa ra trong lợi í ch của ngôn ngƣ̃ đị nh kiểu tƣ̀ một quan điểm kỹ thuật [3]: - Tính kinh tế của việc thƣ̣c hiện : Thông tin kiểu lần đầu tiên đƣợc giới thiệu trong chƣơng trì nh để cải thiện hệ mã và hiệu quả thời gian chạy cho tí nh toán số , ví dụ nhƣ trong FORTRAN . Trong ML thông tin kiểu chí nh xác giúp loại bỏ sƣ̣ kiểm tra cần thiết con số 0 . Nói chung, thông tin kiểu chí nh xác tại thời gian biên dị ch dẫn đến việc áp dụng các phép toán thích hợp thời gian chạy mà không cần chi phí kiểm thử. - Kinh tế cho phát triển qui mô nhỏ : Khi một hệ thống kiểu đƣợc thiết kế tốt, việc kiểm tra kiểu có thể lắm bắt phần lớn lỗi lập trì nh thƣờng xuyên , loại bỏ các phiên gỡ lỗi . Các lỗi xảy ra đƣợc dễ dàng gỡ lỗi , đơn giản chỉ vì các phân lớp lớn của lỗi đƣợc loại trƣ̀. Hơn nƣ̃a các lập trì nh viên giàu kinh nghiệm áp dụng một phong cách mã hóa gây ra một số lỗi logic hiển thị nhƣ các lỗi trong quá trì nh kiểm tra kiểu : Họ sử dụng các bộ công cụ kiểm tra kiểu n hƣ một công cụ phát triển . Cho ví dụ , bằng cách thay đổi tên một trƣờng khi miền bất biến của nó thay đổi mặc dù kiểu của nó vẫn là nhƣ nhau , khi đó ta có đƣợc các thông báo lỗi trên tất cả nhƣ̃ng cái sƣ̉ dụng nó. - Kinh tế về mặt biên dị ch : Thông tin kiểu có thể đ ƣợc tổ chức trong các giao diện giao tiếp giữa các module chƣơng trình . Các module sau đó có thể đƣợc biên dịch độc lập với nhau, với mỗi module chỉ tùy thuộc vào giao diện của các module khác . Việc biên dịch các hệ thống lớn đƣợc thƣ̣c hiện hiệu quả hơn vì í t nhất khi các giao diện ổn đị nh, thay đổi một modul e không làm cho các modul e khác phải biên dịch lại . Kinh tế của việc phát triển quy mô lớn . Các giao diện và các module có phƣơng thức log ic thuận lợi cho phát triển mã . Một nhóm lớn các lập trì nh viên có thể thống nhất chung về mặt giao diện sau đó tiến hành một cách riêng biệt để thƣ̣c hiện mã tƣơng ƣ́ng tƣ̀ng module. Phụ thuộc giữa các phần của mã đƣợc g iảm thiểu và mã bên trong mỗi module có thể đƣợc các sắp xếp lại mà không ảnh hƣởng đến mã toàn cục. - Kinh tế của các tí nh năng ngôn ngƣ̃: Cấu trúc kiểu là đƣợc tạo tƣ̣ nhiên theo các hƣớng trƣ̣c giao. Ví dụ, Pascal một mả ng của các mảng mô hình mảng hai chiều hoặc trong ML một thủ tục với một đối số duy nhất là một bộ n các tham số mô hình một thủ tục của n đối số . Vì vậy hệ thống kiểu thúc đẩy trực giao của các tính năng ngôn ngữ , có xu hƣớng giảm bớt sƣ̣ phƣ́c tạp của ngôn ngƣ̃ lập trì nh. 16 1.1.5. Hệ thống kiểu trong việc chính thức hóa ngôn ngữ kiểu Nhƣ chúng ta đã thảo luận , các hệ thống kiểu đƣợc sƣ̉ dụng để khẳng định ngôn ngữ định kiểu là tốt (well-type), bản thân nó là tĩnh với hành xử đúng và nó đảm bảo chƣơng trình là an toàn. An toàn tạo điều kiện gỡ lỗi bởi hành vi ngăn chặn lỗi của nó. Nhƣng làm thế nào chúng ta có thể đảm bảo rằng các chƣơng trình định kiểu tốt là đang thƣ̣c sƣ̣ hành xƣ̉ đúng? Đó là, làm thế nào chúng ta có thể chắc chắn rằng các qui tắc kiểu của một ngôn ngữ vô tình cho phép các chƣơng trình hành xử kém thông qua? Khi một hệ thống kiểu đƣợc chí nh thƣ́c hóa , chúng ta có thể cố gắng để chứng minh tính đúng đắn định lý kiểu , các chƣơng trình kiểu tốt đƣợc hành xử đúng . Nếu nhƣ tính đúng đắn của định lý đạt đƣợc chúng ta nói rằng hệ thống kiểu là đúng đắn . Tới đây ta có thể cho rằng , hành xử đúng của tất cả các chƣơng trình của một ngôn ngữ định kiểu và tính đúng đắn của hệ thống kiểu của nó có nghĩa giống nhau. Việc chính thức hóa một hệ th ống kiểu là một pha trong chính thức hóa toàn bộ ngôn ngƣ̃ định kiểu. Mỗi một ngôn ngữ có bộ mô tả cú pháp của riêng nó. Qua bộ cú pháp thể hiện các thành phần đặc trƣng trong một chƣơng trình phần mềm và các kiểu của các thành phần đó. Các kiểu thể hiện hiểu biết tĩnh về chƣơng trình , trong khi các thành phần (các câu lệnh, biểu thƣ́c và các đoạn chƣơng trình khác) thể hiện hành vi của thuật toán. Hầu hết các ngôn ngƣ̃ kiểu phân tách rõ ràng hai pha tĩ nh và động của quá trì nh xƣ̉ lý. Pha tĩ nh, chính thức hóa hệ thống kiểu, chƣ́a các phân tí ch và kiểm tra kiểu để đảm bảo rằng chƣơng trình là thiết lập đúng (well-formed); pha động bao gồm các mô tả thƣ̣c thi các chƣơng trì nh thiết lập đúng. Một ngôn ngƣ̃ đƣợc nói là an toàn khi các chƣơng trình thiết lập đúng là hành xử đúng (well-behaved) khi thƣ̣c thi. - Pha tĩ nh (static phase): Đƣợc đặc tả bở i các thành phần tĩ nh bao gồm một tập các qui tắc xuất phát tƣ̀ các đánh giá kiểu với một biểu thƣ́c nói riêng và một chƣơng trình nói chung có đƣợc thiết lập đúng hay không. Phạm vi kiểu cần cho các ngôn ngƣ̃ kiểu là tĩ nh , các ràng buộc vị trí của các đị nh danh phải đƣợc xác đị nh trƣớc thời gian chạy . Các vị trí ràng buộc có thể thƣờng đƣợc xác đị nh hoàn toà n tƣ̀ cú pháp của ngôn ngƣ̃ mà không có bất kỳ phân tí ch sâu hơn , phạm vi tĩnh sau đó đƣợ c gọi là phạm vi tƣ̀ vƣ̣ng . Phạm vi có thể đƣợc đặc tả chí nh thƣ́c bởi xác đị nh các thiết lập các biến tƣ̣ do của một đoạn chƣơng trì nh (liên quan đến việc xác đị nh biến bị ràng buộc nhƣ thế nào bởi các khai báo). Chúng ta có thể tiến hành đị nh nghĩ a các qui tắc kiểu của ngôn ngƣ̃ mô tả một mối quan hệ có kiểu của dạng M:A giƣ̃a các thành phần M và các kiểu A. Một vài ngôn ngữ cũng yêu cầu một mối liên quan kiểu con theo dạng A<:B giƣ̃a các 17 kiểu và thƣờng một mối liên hệ kiểu tƣơng đƣơng đƣợc qui ƣớc A≅B. Tập các qui tắc kiểu của ngôn ngƣ̃ tạo thành hệ thống kiểu. Các qui tắc kiểu không thể đƣợc chính thức hóa mà không cần các thành phần cơ bản đầu tiên đƣợc phản ánh trong cú pháp của ngôn ngƣ̃ , nói cách khác là trong môi trƣờng kiểu . Chúng đƣợc sử dụng để lƣu các kiểu của các biến tự do trong quá trì nh xƣ̉ lý các đoạn chƣơng trì nh , chúng tƣơng ứng chặt chẽ với các bảng ký hiệu (TOKEN table) của một trình biên dịch trong pha kiểm tra kiểu . Các quy tắc kiểu đƣợc xây dƣ̣ng với một môi trƣờng cho đoạn chƣơng trì nh sẽ đƣợc kiểm tra kiểu. Cho ví dụ , có mối quan hệ kiểu M:A là liên kết với môi trƣờng tĩnh 𝛤 chƣ́a thông tin về các biến tƣ̣ do M. Mối liên hệ đƣợc viết đầy đủ là 𝛤 ⊢ 𝑀: 𝐴, có nghĩa là M có kiểu A trong môi trƣờng 𝛤. - Pha động (dynamic phase) của một ngôn ngữ là một mô tả chƣơng trìn h đƣợc thƣ̣c hiện nhƣ thế nào . đị nh nghĩ a các ngƣ̃ nghĩ a nhƣ một ràng buộc có giá trị giƣ̃a các thành phần và tập các kết quả . Các quan hệ hình thƣ́c này phụ thuộc mạnh mẽ vào phong cách của các ngƣ̃ nghĩ a đƣợc thông qua . Trong bất kỳ trƣờng hợp nào , các ngƣ̃ nghĩ a và hệ thống kiểu của một ngôn ngƣ̃ đƣợc kết nối với nhau. Hệ thống kiểu đƣợc cài đặt nhƣ một phần của trình biên dịch trong ngôn ngữ [10]. Nó trong bộ Semantic routine sau trạng thái Syntactic analysis nhƣ ở Hình 1.1: Hình 1.1 Hệ thống kiểu trong trình biên dịch[10] Có 3 trạng thái của trình biên dịch: scanning, syntactic analysis và type analysis có thể xem nhƣ ba thành chức năng: scanner, parser, typechecker. Đầu vào là chƣơng trình mà các lập trình viên xây dựng từ các ngôn ngữ lập trình. scanner sử dụng hữu hạn các trạng thái và ánh xạ chuỗi ký tự vào bảng TOKEN. Bằng việc sử dụng một vài thuật toán, parser ánh xạ bảng TOKEN vào một cấu trúc trừu tƣợng của chƣơng trình (thƣờng là một cây cú pháp trừu tƣợng). Một ngôn ngƣ̃ kiểu có thể hành xƣ̉ tốt (chƣ́a đƣ̣ng tính an toàn ) bằng cách thƣ̣c hiện kiểm tra tĩ nh (tƣ́c là kiểm tra trƣớc ở thời điểm biên dị ch chƣơng trình sang mã máy) để ngăn chặn các chƣơng trình không an toàn và hành xử kém trong từng lần chạy . Các 18 mã chƣơng trình đƣợc kiểm tra tĩ nh, quá trình kiểm tra đƣợc gọi là quá trình kiểm tra kiểu và bộ các thuật toán thực hiện kiểm tra này gọi là bộ kiểm tra kiểu (type checker). Một chƣơng trì nh khi đƣợc thông qua bởi bộ kiểm tra kiểu đƣợc gọi là kiểu tốt (well typed), ngƣợc lại, là kiểu yếu (ill typed), có nghĩa rằng nó nó hành xử yếu hoặc đơn g iản là nó không đảm bảo hành xƣ̉ tốt . Typechecker đƣa các kiểu vào cấu trúc cú pháp trừu tƣợng. Typechecker là một thành phần gọi là semantic subroutine của bộ biên dịch. Và phần thực nghiệm của chúng ta ở Chƣơng 4, ta sẽ đi xây dựng một dạng Typechecker, kiểm tra và tính kiểu cho một chƣơng trình nguồn TFJ. 1.2. Bộ nhớ giao tác phần mềm 1.2.1. Khái niệm và các thuộc tính cơ bản của giao tác Giao tác (transaction) là tập hợp thứ tự các thao tác tạo thành một đơn vị làm việc logic thỏa mãn hoặc thƣ̣c hiện đầy đủ hoặc là hủy bỏ hoàn toàn. Hiện nay khái niệm giao tác đƣợc tí ch hợp phổ biến vào trong các bộ máy làm việc của các ngôn ngữ lập trình để cung cấp các giá trị an toàn và đảm bảo các thuộc tí nh nhƣ tính nguyên tử, nhất quán, độc lập, bền vƣ̃ng đƣợc viết tắt là ACID [16] : - Tính nguyên tử (atomicity): Một giao tác là một chuỗi các thao tác đƣợc thƣ̣c thi một cá ch nguyên tƣ̉ , hoặc toàn bộ đƣợc thƣ̣c hiện hoặc không . Một giao tác đƣợc gọi là thành công khi nó thực hiện toàn bộ hoạt động (commit), ngƣợc lại nó sẽ bị hủy bỏ (abort). - Tính nhất quán (consistency): Tất cả các giao tác có cùng cách nhìn về dữ liệu đƣợc chia sẻ. - Tính độc lập (isolation): Khi một giao tác đang thƣ̣c hiện thì các giao tác khác không đƣợc phép can thiệp vào quá trì nh thƣ̣c hiện của nó (tức là không có tình huống một phần công việc của giao tác này sẽ làm một phần công việc của giao tác khác). - Tính bền vững (durability): Các trạng thái thay đổi sau khi thƣ̣c hiện thành công luôn đƣợc duy trì . Hình 1.2 Sơ đồ các trạng thái của giao tác 19 Hoạt động của giao tác đƣợc mô tả trong sơ đồ trạng thái ở Hình 1.2. Giao tác đƣợc bắt đầu với trạng thái Active với thao tác mở giao tác (onacid), sau đó nó có thể thực hiện các thao tác đọc , ghi các mục dữ liệu , kết thúc thao tác cuối cùng trong giao tác thì giao tác chuyển tới trạng thái Partially Commit (cam kết cục bộ). Ở trạng thái này giao tác chƣa thực sự hoàn tất hoàn toàn mặc dù nó đã th ực thi hết các thao tác , bởi lẽ kết quả đầu ra của nó có thể đƣợc lƣu trú trên bộ nhớ chí nh , do vậy khi có một sƣ̣ cố về phần cƣ́ng (bộ nhớ chí nh ) thì giao tác hoàn toàn có thể bị ngăn cản và dẫn tới hủy bỏ . Trong tình huống thuận lợi không có sƣ̣ cố xảy ra đối với trạng thái Partially Commit thì giao tác đi vào trạng thái Commit (hay gọi là cam kết ). Tại trạng thái này giao tác đƣợc hoàn tất, kết quả sẽ đƣợc bảo toàn và duy trì (thể hiện tí nh bền vƣ̃ng ). Không phải bất kỳ giao tác nào cũng thực hiện mà không thể xảy ra sự cố , do vậy khi xảy ra một sƣ̣ cố làm cho giao tác không thể thƣ̣c hiện đƣợc nƣ̃a thì khi đó giao tác sẽ ở trạng thái Failed. Đối với nhƣ̃ng trƣờng hợp giao tác bị Failed để đảm bảo tính nguyên tử và tất cả các dữ liệu đã bị biến đổi trong quá trì nh thƣ̣c hiện cho tới thời điểm Failed thì giao tác cần phải khôi phục trạng thái (Rollback) trƣớc khi khở i động, cuối của quá trì nh này giao tác đạt trạng thái Abort. 1.2.2. Bộ nhớ giao tác phần mềm Nhƣ chúng ta đã nói ở phần giới thiệu, bộ nhớ giao tác phần mềm, Software Transactional Memory (viết tắt là STM), đƣợc xem nhƣ một giải pháp viết các chƣơng trình song song, thay cho cơ chế đồng bộ hóa dựa trên khóa (lock-based synchronization) đối với việc chia sẻ bộ nhớ đồng thời [12]. Trong đó mỗi giao tác cho phép tự do đọc và ghi để chia sẻ các biến và một log đƣợc sử dụng để ghi các hoạt động này cho tới thời điểm commit [15]. Một trong các mô hình giao tác gần đây hỗ trợ tính năng cao cấp nhƣ giao tác lồng và đa luồng (nested and multi-threaded transactions) đƣợc mô tả trong [10]. Trong mô hình này, một giao tác đƣợc lồng nếu nó chứa một số các giao tác khác, các giao tác con, các giao tác con này phải đƣợc commit trƣớc giao tác cha của chúng. Hơn nữa, một giao tác là multi-threaded khi các luồng đƣợc phép chạy bên trong giao tác và song song với luồng cha đang thực thi giao tác đó. Các luồng sinh ra bên trong một giao tác sẽ kế thừa các giao tác đang mở và sao chép bộ nhớ sử dụng của luồng cha của nó. Khi luồng cha thực hiện commit một giao tác thì tất cả các luồng con phải tham gia commit cùng cha chúng. Chúng ta gọi các commit của các luồng con và luồng cha cùng tham gia đó là các joint commit, tại mỗi thời điểm đó gọi là một điểm joint commit. Vì đồng bộ hóa, các luồng song song bên trong một giao tác không chạy độc lập. Mỗi giao tác có bản sao bộ nhớ cục bộ của chính nó đƣợc gọi là log để lƣu giữ bộ nhớ truy cập trong quá trình thực thi. Mỗi luồng có thể thực hiện một số các giao tác và 20 nhƣ thế có thể chứa một số các log. Đặc biệt, một luồng con cũng sẽ lƣu trữ một bản sao các log của cha nó, vì vậy luồng con cũng có thể đƣợc thực thi độc lập với cha của chúng ở các thời điểm khác thời điểm joint commit. Ở thời điểm khi tất cả các luồng con và cha của chúng đồng bộ thông qua các joint commit, các log và bản sao của chúng đƣợc kiểm tra xem có xung đột tiềm tàng nếu có thì tiến hành thực thi rollback. Một vấn đề phức tạp hơn cho phân tích tĩnh là bộ nhớ xác định là hoàn toàn đƣợc sao chép vào trong log cục bộ, tài nguyên đƣợc sử dụng bởi một chƣơng trình giao tác là khó để đánh giá. Một ví dụ đƣợc xem nhƣ minh họa cho mô hình giao tác có tích hợp tính năng giao tác lồng và đa luồng. Cho một đoạn giả mã nhƣ sau: Hình 1.3 Ví dụ giả mã cho mô hình giao tác lồng và đa luồng [17] Trong chƣơng trình minh họa ở Hình 1.3, bắt đầu một giao tác với lệnh onacid và kết thúc giao tác bởi lệnh commit đƣợc ký hiệu bằng [ và ] tƣơng ứng. Lệnh spawn tạo một luồng mới chạy song song với luồng cha. Luồng mới tạo một bản sao các biến cục bộ của luồng cha vào trong môi trƣờng của nó. Trong ví dụ của chúng ta khi sinh 𝑒1 , luồng chính Thread 0 đã mở 2 giao tác, vậy Thread 1 thực hiện 𝑒1 bên trong 2 giao tác này và phải thực hiện 2 commit để đóng chúng. Đó là lý do tại sao sau 𝑒1 , Thread 1 cần thực thi 2 lệnh commit. Hình 1.4 minh họa rằng các luồng song song phải commit một giao tác ở cùng một thời điểm. Hình 1.4 Ví dụ mô hình giao tác lồng, đa luồng và joint[17] Mô hình của chúng ta bàn đến nó phá vỡ ràng buộc giới hạn về ngữ nghĩa của ngôn ngữ đặt ra, giới hạn mà không cho phép các giao tác đƣợc mở bên trong các luồng đã 21 đƣợc sinh ra sau một joint commit với cha chúng, theo [14]. Ở đây chúng ta phát triển một hệ thống kiểu để đánh giá tĩnh tổng chi phí bộ nhớ dành cho chƣơng trình bằng số các log lớn nhất, các log tồn tại ở cùng một thời điểm. Theo ví dụ, giả sử e1 mở và đóng 1 giao tác, e2 mở và đóng 2 giao tác, e3 mở và đóng 3 giao tác, e4 mở và đóng 4 giao tác. Chi phí tài nguyên lớn nhất thể hiện sau khi sinh e2. Ở thời điểm đó, e1 đóng góp 3 giao tác (2 giao tác kế thừa từ Thread 0, 1 giao tác của bản thân), e2 góp 5 giao tác (3 giao tác từ Thread 0 và 2 giao tác là của chính nó), bản thân Thread 0 đóng góp 3 giao tác. Và tổng sẽ là 3+5+3=11 giao tác. Nhƣ đã nhấn mạnh, các luồng song song không hoàn toàn là độc lập. Các luồng con liên kết với luồng cha của chúng thông qua các joint commit ở thời điểm mà một điểm đồng bộ hóa hoàn toàn. Đây cũng là điểm mới mà hƣớng nghiên cứu xem xét đến để cải thiện việc tính toán tổng chi phí tài nguyên, làm sao đƣa ra một lƣợng tổng tài nguyên thực sự sát thực nhất (tức là càng nhỏ càng tốt mà vẫn đáp ứng mọi hoạt động của chƣơng trình) so với các nghiên cứu trƣớc đó [13]. Thật vậy, ta có thể xét một ví dụ sau: Ví dụ 1.4 Cho một mô hình giao tác đơn giản nhƣ hình Hình 1.5 Ví dụ mô hình giao tác thể hiện tính phụ thuộc các luồng song song Áp dụng 1, theo các nghiên cứu trƣớc việc tính toán tài nguyên hoàn toàn dựa trên các luồng song song độc lập. Với luồng thread1 tài nguyên lớn nhất mà nó sử dụng là ở thời điểm maxt1 (có giá trị bằng 4). Mặt khác, với luồng thread 2, tài nguyên lớn nhất nó sử dụng là tại maxt2 (có giá trị bằng 4). Nhƣ vậy, với cách này tổng tài nguyên công lại là maxt1 + maxt2 = 4+4=8. Áp dụng 2, theo lý thuyết có suy xét đến sự phụ thuộc các luồng thông qua các điểm joint commit chúng ta thấy việc cộng dồn trên là hoàn toàn không triệt để và luôn thu đƣợc con số chƣa đạt mức tối ƣu. Thứ nhất, giả sử nếu luồng thread 2 sử dụng đạt đến mức độ maxt1 thì khi đó luồng thread 1 vẫn chƣa sử dụng tài nguyên đạt đến mức maxt2 bởi lẽ lúc đó chƣa xảy ra điểm joint commit 1 (cũng có nghĩa là thread 1 chƣa đóng cả thao tác commit ở thời điểm joint commit 1). Và nhƣ vậy cả 2 thread 1 và thread 2 vẫn đang làm việc ở Phân vùng độc lập 1. Nếu ta gọi S1 là tổng chi phí lớn nhất tại Phân vùng 22 độc lập 1 này thì S1= 3+4 =7. Trong đó, thread 1 đóng góp 3 thao tác mở mà chƣa đóng giao tác, thread 2 đóng góp 4 thao tác mở mà chƣa đóng (2 kế thừa từ cha và 2 của bản thân trong thời điểm lớn nhất). Thứ hai, nếu giả sử rằng thread 2 sử dụng tài nguyên đạt đến mức độ maxt2 thì khi đó luồng thread 1 đã qua giai đoạn sử dụng đến mức tối đa, lúc này nó sử dụng nhỏ hơn (cụ thể là tối đa bằng 2), tức là thread 1 và thread 2 đã đồng loạt qua giai đoạn sau điểm joint commit 1 và sau điểm joint commit 2 (tức là nằm trong Phân vùng độc lập 2). Nếu ta gọi S2 là tổng chi phí tối đa nó phải tiêu tốn thì ta có S2= 4+2 =6, trong đó thread 1 góp 4, thread 2 góp 2. Nhƣ vậy tổng tài nguyên S tổng hợp cho cả mô hình phải là giá trị lớn nhất của tài nguyên tại các phân vùng độc lập, tức là , S = max(S1, S2)=max(7, 6)=7 < 8. Một điều nhận thấy rằng, kết quả thu đƣợc từ Áp dụng 2 luôn luôn nhỏ hơn Áp dụng 1, có nghĩa là con số này nó đã đƣợc tối ƣu. Do đó việc suy xét đến thông tin các luồng phụ thuộc nhau thông qua các điểm joint commit là rất cần thiết trong việc tính toán giới hạn trên chi phí tài nguyên cho chƣơng trình và đây cũng thể hiện mặt hạn chế về phƣơng thức tính toán nhƣ các nghiên cứu trƣớc [13] mà chúng ta đã nói ở trên. Khó khăn cho phân tích là phải bắt đƣợc các điểm đồng bộ ở thời điểm biên dịch, khi cú pháp không đƣợc thể hiện rõ ràng. Hơn nữa, phân tích cần chứa đủ thông tin hợp lệ để phân tích chi phí tài nguyên một cách tổng thể. Tất cả sẽ đƣợc đáp ứng với hệ thống kiểu ở Chƣơng 3. Nói tóm lại, trong Chƣơng 1 chúng ta tìm hiểu một số quan điểm về khái niệm hệ thống kiểu, các thuộc tính và vai trò của hệ thống kiểu trong ứng dụng sản xuất phần mềm. Đồng thời chúng ta cũng nghiên cứu vị trí của hệ thống kiểu trong giai đoạn xây dựng chính thức hóa ngôn ngữ kiểu. Đây cũng là khối kiến thức ban đầu, nền tảng cho các lý thuyết và thực nghiệm của các chƣơng về sau. Trong chƣơng tiếp theo chúng ta sẽ giới thiệu cú pháp cũng nhƣ ngữ nghĩa của ngôn ngữ có sử dụng yếu tố giao tác.