Luận văn -Xây dựng hệ thống giải bài toán Satisfiability Modulo Theories(SMT) hiệu năng cao – phần máy trạm

(6) ::= :sort ( +) | :funs (+) | :preds () | :definition | :axioms | (7) ::= (theory +) Bảng 4: Luật sinh một logic (1) ::= (2) ::= : theory | :language | :extensions | :notes Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 9 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng | (3) ::= (logic +) Bảng 5 Luật sinh một chuẩn (1) ::= sat | unsat | unknown (2) ::= (3) ::= :logic | :assumption | :formula | :status | :extrasorts ( + ) | :extrafuns ( + ) | :extrapreds ( + ) | :notes | (4) benchmark ::= ( benchmark + ) Các lý thuyết nền cơ bản đã được nghiên cứu và đưa ra: Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2 Arrays Các hàm mảng ArraysEx Các hàm mảng mở rộng Fixed_Size_BitVectors[32] Bit vector 32 bit Fixed_Size_BitVectors Bit vector với kích cỡ tùy ý. BitVector_ArraysEx Bit vector với kích cỡ tùy ý và mảng chứa kiểu dữ liệu bit vector Empty Thuyết trống với ký hiệu rỗng Ints Số nguyên Int_Arrays Mảng số nguyên Int_ArraysEx Mảng giá trị được đánh thứ tự số nguyên với tiền đề mở rộng Int_Int_Real_Array_ArraysEx Mảng của mảng các số nguyên và số thực với tiền đề mở rộng Reals Số thực Reals_Ints Số nguyên và số thực Nội dung cụ thể của từng lý thuyết xin được không đề cập đến ở đây để tránh việc trình bày lan man không cần thiết. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 10 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Các logic cơ bản được áp dụng trong định dạng của SMT-LIB: Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2 AUFLIA Các công thức tuyến tính trên thuyết mảng số nguyên với những ký tự phân cấp, hàm và thuộc tính tự do. AUFLIRA Các công thức tuyến tính với ký hiệu hàm và ký hiệu vị từ trong thuyết 10 nêu trên AUFNIRA Công thức với các ký tự hàm và vị từ tự do dựa trên thuyết 10 LIA Công thức tuyến tính trên các phép toán số nguyên LRA Công thức tuyến tính trên các phép toán số thực QF_A Công thức lượng từ tự do trên thuyết mảng không mở rộng QF_AUFBV Công thức lượng tự trên thuyết bitvector và mảng bitvector với các ký hiệu hàm và ký hiệu vị từ tự do. QF_AUFLIA Công thức tuyến tính và lượng từ tự do trên thuyết mảng các số nguyên với ký tự phân cấp, ký tự hàm và ký tự lượng từ. QF_AX Công thức lượng từ tự do trên thuyết của mảng mở rộng QF_BV Công thức lượng từ tự do với thuyết bitvector cố định kích cỡ QF_IDL Logic khác trên số nguyên. Ví dụ bất đẳng thức x-y <b với x,y là các biến nguyên và b là một hằng số nguyên QF_LIA Tổ hợp giữa bất đẳng thức của đa thức tuyến tính trên biến số nguyên QF_LRA Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số thực QF_NIA Tổ hợp bất đẳng thức giữa đa thức tuyến tính trên biến số nguyên với ít nhất một đa thức không tuyến tính QF_RDL Logic khác của số thực, ví dụ bất đẳng thức x – y < b với x,y là số thực và b là một hằng số hữu tỷ QF_UF Công thức vô lượng hóa (Unquantified formulas) xây dựng trên ký hiệu của ký tự phân cấp, ký tự hàm, ký tự vị từ không QF_UFIDL Logic khác trên số nguyên nhưng với những ký tự phân cấp, ký tự hàm, ký tự vị từ không được giải thích QF_UFBV Công thức vô lượng hóa trên kiểu bitvectors với ký tự hàm và ký tự vị từ. QF_UFLIA Phép tính số nguyên vô lượng hóa tuyến tính với ký tự phân cấp, ký tự hàm và ký tự vị từ QF_UFLRA Phép tính số thực vô lượng hóa tuyến tính với ký tự phân cấp, ký tự hàm và ký tự vị từ QF_UFNRA Phép tính số thực vô lượng hóa không tuyến tính với ký tự phân cấp, ký tự hàm và ký tự vị từ Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 11 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng UFNIA Phép tính số nguyên không tuyến tính với ký tự phân cấp, hàm và vị từ không xác định. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Chương 3. Phân tích hệ thống 3.1. Mô hình hệ thống Để giải một bài toán SMT một cách song song giữa các bộ giải, đồng thời đảm bảo được hiệu năng cao cho hệ thống, nhóm nghiên cứu đã đưa ra hướng giải quyết là xây dựng hệ thống giải quyết vấn đề SMT trực tuyến qua mạng. Hệ thống sẽ được chia ra làm ba phần rõ rệt là phần máy khách gửi yêu cầu giải quyết vấn đề, phần máy chủ xử lý và phân phối các vấn đề nhận được, và phần máy trạm giải quyết vấn đề được yêu cầu. Mô hình hệ thống được xây dựng như sau: Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao. Việc xây dựng phát triển hệ thống giải quyết vấn đề SMT trực tuyến sẽ đáp ứng được yêu cầu về hiệu năng xử lý đầu vào. Hệ thống sẽ tiếp nhận một lúc nhiều vấn đề Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 13 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng từ nhiều người sử dụng trực tuyến. Với mỗi vấn đề nhận được, hệ thống sẽ phân phối cho tất cả các bộ giải và chờ đợi kết quả trả về tối ưu nhất về mặt thời gian để trả về cho phía yêu cầu. Đối với những bộ giải đưa ra kết quả sau sẽ nhận được tín hiệu dừng xử lý vấn đề đó. Do hệ thống được xây dựng trực tuyến, nên việc nhận cùng một lúc nhiều yêu cầu cần xử lý là điều tất yếu, vì vậy, hệ thống máy chủ vừa đảm nhận việc chia một vấn đề cho nhiều máy trạm xử lý, vừa phải xử lý đồng thời cùng lúc nhiều yêu cầu như vậy. Về phía máy trạm, mỗi máy trạm sẽ luôn nhận và xử lý nhiều các vấn đề một lúc và phải trả về kết quả tương ứng cho mỗi vấn đề. Để tiện cho người sử dụng bên phía máy khách, hệ thống cần phải có một thư việc các hàm nhúng API để người sử dụng trực tiếp xây dựng vấn đề SMT và gửi lên phía máy chủ. 3.2. Mô hình ca sử dụng của hệ thống Đối với hai hệ thống con được cài đặt trên máy khách và máy trạm, thì máy chủ được coi như là một tác nhân trung gian giúp duy trì tương tác giữa chúng với nhau. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Hình 3.2: Mô hình ca sử dụng của hệ thống Ở phía máy khách (user), người sử dụng sẽ tạo bài toán SMT, hoặc chỉ định cho hệ thống tệp tin SMT cần thiết phải kiểm tra tính thỏa mãn để hệ thống sẽ gửi lên phía máy chủ (server). Sau khi gửi bài toán lên phía máy chủ, hệ thống trên máy khách sẽ chờ cho máy chủ gửi kết quả về và nhận kết quả trả về. Viêc gửi bài toán SMT bên phía máy khách sẽ bao gồm cả việc gửi yêu cầu thời gian ngắt của các bộ giải SMT. Với máy trạm (solver) sau khi kết nối và nhận được tệp tin chứa vấn đề SMT cần giải quyết, hệ thống sẽ gọi lệnh chạy các công cụ giải SMT. Sau khi đưa ra được kết quả, hoặc sau khi nhận được tín hiệu ngắt từ phía máy chủ, máy trạm sẽ gửi lại kết quả đến máy chủ để máy chủ gửi lại phía máy khách. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 3.3. Mô hình hoạt động Hình 3.3: Mô hình hoạt động của hệ thống Từ biểu đồ hoạt động của hệ thống, ta có thể xác định được các công việc tuần tự của hệ thống và cách làm việc của hệ thống như sau: Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 16 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Khi hệ thống hoạt động, các máy khách sẽ kết nối đến máy chủ và xây dựng bài toán SMT. Bài toán SMT có thể đã được mô tả bằng tệp tin hay được xây dựng bằng chương trình với việc sử dụng hệ thống được cài đặt trên. Sau khi xác định bài toán SMT, hệ thống máy khách sẽ gửi bài toán toán đó cho máy chủ đồng thời gửi thông tin về thời gian giới hạn thực hiện giải bài toán và chờ đợi kết quả trả về từ phía máy chủ. Máy chủ lắng nghe các kết nối của máy khách, khi nhận được bài toán SMT và tham số về thời gian thực hiện bài toán gửi từ máy khách, máy chủ sẽ phân phối các bài toán đó cho các máy trạm có bộ giải các bài toán SMT đang kết nối đến máy chủ và đón chờ kết quả phản hồi từ máy trạm. Máy trạm sẽ nhận bài toán từ máy chủ và bắt đầu việc thực hiện giải bài toán, khi đó giá trị về trễ thời gian cho mỗi bài toán sẽ được sử dụng. Sau khi hệ thống trên máy trạm gọi các bộ giải để giải quyết vấn đề được đưa tới, sẽ có hai trường hợp xảy ra tiếp sau đó. Trường hợp một là máy trạm đó sẽ giải ra kết quả nhanh nhất và gửi về phía máy chủ kết quả. Trường hợp thứ hai là nhận được tín hiệu ngắt tiến trình (do đã có máy trạm khác gửi được kết quả đến máy chủ), khi đó, một lệnh ngắt tiến trình đang được thực thi sẽ được gọi. Và ở trường hợp này, máy trạm không gửi gì về phía máy chủ nữa. Phía máy khách sau khi nhận được kết quả của hệ thống sẽ hiển thị cho người dùng thấy được kết quả của bài toán mà hệ thống gửi đến. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 17 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Chương 4. Phương hướng giải quyết vấn đề 4.1. Lựa chọn phương thức kết nối Bài toán được đặt ra là xây dựng hệ thống trực tuyến, vì vậy cần có phương thức kết nối phù hợp với những yêu cầu đã được nêu ra trong phần trên. Có hai phương thức kết nối được đưa ra lựa chọn là xây dựng hệ thống dựa trên các kết nối của webservice hoặc sử dụng kết nối socket. Đối với phương thức kết nối dựa trên webservice, thời gian kết nối sẽ chậm hơn rất nhiều so với kết nối trực tiếp qua socket. Tuy nhiên, với phương thức kết nối socket, ta phải tự xây dựng cách thức giao tiếp giữa máy trạm với máy chủ và máy chủ với máy khách. Do yêu cầu tối ưu về mặt thời gian được quan tâm hàng đầu, vì vậy phương thức được tối ưu cho hệ thống là xây dựng giao tiếp qua kết nối socket. 4.2. Lựa chọn ngôn ngữ lập trình Do phương thức kết nối được lựa chọn là kết nối socket, vì vậy cần một ngôn ngữ lập trình bậc cao để tiện cho việc xây dựng cách thức giao tiếp giữa máy chủ - máy trạm và máy chủ - máy khách. Mặt khác, do các bộ giải có thể được cài đặt trên nhiều nền hệ điều hành khác nhau, nên cần có ngôn ngữ lập trình hỗ trợ việc chạy trên nhiều hệ điều hành khác nhau. Chính vì các lý do này, nhóm nghiên cứu đã quyết định sử dụng ngôn ngữ lập trình Java để xây dựng hệ thống. 4.3. Xác định dữ liệu đầu vào, đầu ra của hệ thống Để tăng hiệu năng của hệ thống giải bài toán SMT, hệ thống có sử dụng nhiều các bộ giải khác nhau. Tuy rằng mỗi bộ giải có một chuẩn đầu vào riêng, nhưng để tiện cho việc giải quyết vấn đề một cách nhanh chóng và hiệu quả, hệ thống chỉ sử dụng đầu vào bài toán SMT theo chuẩn của SMT-LIB. Hiện nay, hầu hết các công cụ giải các bài toán đều hỗ trợ chuẩn SMT-LIB, vì vậy, để tránh việc phải chuẩn hóa đầu vào cho mỗi bài toán nhằm đảm bảo hiệu năng cao về mặt thời gian, hệ thống yêu cầu Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 18 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng đầu vào của người sử dụng phải đáp ứng nghiêm ngặt các điều kiện xây dựng một bài toán dưới quy chẩn của SMT-LIB. Hệ thống được chia ra thành ba thành phần với chức năng và vai trò khác nhau, do đó với mỗi hệ thống con sẽ có một đầu vào đầu ra riêng ứng với từng chức năng của hệ thống con đó. Với hệ thống được cài đặt trên máy khách, người dùng sẽ đưa vào tệp tin chứa bài toán SMT hoặc xây dựng bài toán SMT dựa trên các hàm nhúng API mà hệ thống xây dựng. Bài toán sẽ được gửi lên máy chủ và chờ máy chủ phản hồi về kết quả. Đối với hệ thống được cài đặt trên máy chủ, đầu vào nhận từ máy khách (bài toán SMT) sẽ là đầu ra chuyển tới máy trạm. Và đầu vào thứ hai là kết quả nhận được từ máy trạm cũng là đầu ra để chuyển tới máy khách. Trên máy trạm có duy nhất một bộ dữ liệu đầu vào là bài toán SMT nhận được từ máy chủ và một bộ dữ liệu đầu ra duy nhất là kết quả của việc giải bài toán SMT đó. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 19 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Chương 5. Mô tả hệ thống Hệ thống giải bài toán SMT hiệu năng cao được chia làm ba hệ thống con với chức năng và tác dụng riêng. Trong giới hạn tài của tài liệu này, hệ thống con cài đặt trên máy chủ sẽ không được đề cập đến. Trong phần này, hệ thống cài đặt trên máy khách và máy trạm sẽ đươc giải thích và mô tả chi tiết. 5.1. Quy định cách thức giao tiếp với máy chủ Do hệ thống hoàn toàn được xây dựng bằng phương pháp kết nối socket, vì vậy cần phải có một cách thức giao tiếp phù hợp giữa các hệ thống con với nhau. Dựa trên ý tưởng của ngôn ngữ XML, nhóm nghiên cứu đã đưa ra và thống nhất việc sử dụng các thẻ đươc quy định sẵn để giao tiếp giữa các hệ thống con với nhau. Các thẻ sẽ được định nghĩa đúng như quy chuẩn của XML với quy định sau: - Thẻ mở sẽ có dạng - Thẻ đóng sẽ có dạng Đối với thẻ đơn thì không cần có thẻ đóng. Cụ thể, các thẻ được quy định trong hệ thống như sau: - Cặp thẻ : thể hiện sự bắt tay kết nối giữa các thành phần trong hệ thống với nhau. - Cặp thẻ : thể hiện việc bắt đầu chuyển dữ liệu từ tệp tin chứa bài toán SMT giữa các hệ thống con trong hệ thống - Cặp thẻ : thể hiện nội dung kết quả của bài toán SMT được trả về - Thẻ đơn : là tín hiệu ngắt kết nối được máy chủ gửi đến máy trạm - Thẻ đơn : thể thiện sự kết thúc kết nối giữa người dùng với máy chủ Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 20 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.2. Phần máy khách 5.2.1. Quy định giao tiếp với máy chủ Yêu cầu chính cho hệ thống cài đặt trên máy khách là gửi bài toán SMT và nhận về kết quả của bài toán ấy. Quy trình kết nối của máy khách với máy chủ sẽ như sau: - Sau khi kết nối được máy chủ, máy khách sẽ đưa ra một loạt thẻ chào hỏi [Name] - Sau chuỗi các thẻ được gửi lên máy chủ, máy khách sẽ chờ đến khi máy chủ đáp lại “OK”. Sau đó, hệ thống trên máy khách sẽ thực hiện tiến trình gửi trễ thời gian (time out) giải bài toán SMT cần giải. Trễ thời gian này được người sử dụng quy định và đưa vào.Trong trường hợp người dùng không thiết lập thông tin này, thì hệ thống sẽ gửi lên thời gian mặc định là 30 giây. Quá trình gửi trễ thời gian được quy định như sau: [trễ thời gian] - Sau khi gửi lên thời gian giới hạn thực thi của bài toán, hệ thống sẽ tiếp tục gửi lên tệp tin dữ liệu chứa nội dung bài toán. Quy trình gửi tệp tin dữ liệu cũng được theo quy định sau: [Nội dung dữ liệu chuyển lên] - Sau quá trình gửi tệp tin dữ liệu thành công, hệ thống trên máy khách chờ kết quả của máy chủ trả về. Khi nhận được tín hiệu trả về ( tín hiệu kết quả trả về được quy định là thẻ mở ) hệ thống sẽ nhận cho đến khi có tín hiệu kết thúc (thẻ đóng ): [nội dung kết quả trả về] Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 21 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng - Sau khi đã nhận được kết quả, máy khách sẽ chủ động ngắt kết nối đến máy chủ. Như đã đề cập ở trên, để tránh việc lãng phí thời gian của hệ thống cho việc chuẩn hóa đầu vào, hệ thống yêu cầu người sử dụng đưa vào đầu vào theo đúng chuẩn của SMT-LIB. Vấn đề đặt ra ở đây là không phải lúc nào người sử dụng cũng có sẵn bài toán SMT được tổ chức theo quy chuẩn của STM-LIB. Chính vì vậy, hệ thống cần phải xây dựng các hàm API để người dùng có thể xây dựng bài toán theo đúng chuẩn định dạng của SMT-LIB. Dựa vào các định nghĩa và quy chuẩn về đầu vào của bài toán SMT theo chuẩn SMT-LIB (được nêu trong phần kiến thức nền tảng), hệ thống đã đưa ra các hàm API để thuận tiện cho người sử dụng đưa vào. 5.2.2. Các lớp của hệ thống máy khách 5.2.2.1. Lớp config: lớp này được xây dựng để chứa các quy ước việc giao tiếp cũng như các thành phần mặc định của hệ thống như các thẻ, tên tệp tin đầu vào mặc định, thời gian ngắt mặc định, tên tệp tin chứa dữ liệu được trả về 5.2.2.2. Lớp Client: Có chức năng mở kết nối, gửi bài toán từ tệp tin lên máy chủ và nhận về kết quả. 5.2.2.3. Lớp NetSolver: bao gồm các hàm thiết lập tùy chọn cho người sử dụng. Cụ thể: - void setPath (String Path): Thiết lập đường dẫn cho tệp tin đầu vào. Có thể là một đường dẫn đến một tệp tin sẽ được xây dựng sau đó bởi chính người sử dụng. Hoặc cũng có thể là một tệp tin đã chứa nội dung bài toán SMT cân gửi lên máy chủ. - void setOutput (String Path): Thiết lập đường dẫn cho tệp tin lưu giữ kết quả được trả về. Xin lưu ý rằng việc thiết lập đường dẫn bao gồm cả tên tệp tin. - void Solve (): thực thi việc gửi và nhận bài toán SMT. Thực chất hàm này chỉ gọi một đối tượng của lớp Client và thực thi đối tượng ấy. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 22 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Việc xây dựng bài toán SMT sẽ dựa trên các hàm API được xây dựng bởi các lớp sau. Xin lưu ý rằng các hàm API được xây dựng hoàn toàn dựa trên bộ luật cú pháp của ngôn ngữ đầu vào SMT đã được đưa ra ở trên. 5.2.2.4. Lớp Bench_attribute: Được xây dựng dựa trên bảng 5. - Bench_attribute (String Bench_name) : Định nghĩa một thuộc tính Benchmark đầu vào với tên là Bench_name. - Void setLogic (String LogicName): thiết lập tên logic của Benchmark - void setStatus (String stt) : thiết lập thuộc tính Status cho Benchmark - void setFormulas (Formula F): thiết lập Formula cho Benchmark. - void setAssumtion (Formula f): thiết lập Assumtion cho Benchmark - void setAnnotation (annotation an): thiết lập Annotation cho Benchmark - void setNotes (String note): thiết lập Note cho Benchmark - void setExtrasorts (Identifier[] id): Thiết lập Extrasorts cho Benchmark - void setExtrafuns (func_decl[] funcs): Thiết lập Extrafuns cho Benchmark - void setExtrapreds (pred_decl[] preds): thiết lập Extrapreds cho Benchmark - void printBench (): ghi Benchmark vừa thiết lập ra tệp tin được chỉ định 5.2.2.5. Lớp Formula: Được xây dựng dựa trên bảng 2 để đưa ra các công thức trong bài toán SMT, Các hàm hỗ trợ xây dựng bao gồm: - Formula (boolean b): khai báo một Formula với giá trị là giá trị của một biến logic - Formula (fvarDecl fvar): Khai báo một Formula với giá trị là một khai báo hàm. - Formula (Identifier id): khai báo một Formula với giá trị là một định danh Identifier. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 23 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng - Formula (Identifier id, Term te[]): khai báo một Formula từ một định danh Identifier và một mảng không rỗng các phần tử Term - Formula (Arith_symb ar, Term te[]): khai báo một Formula từ một (hoặc một chuỗi) các phép toán và một mảng không rỗng các phần tử Term - Formula (Term te[]): khai báo một Formula với từ khóa “distinct” và một mảng không rỗng các phần từ Term - void Setvalue (String val): đặt giá trị của Formula theo tùy biến ( khi công thức của người sử dụng không thể xây dựng dựa trên các hàm API trong lớp formula) - Formula orOperator (Formula a1, Formula a2): phép “or” giữa hai công thức - Formula xorOperator (Formula a1, Formula a2): phép “xor” giữa hai công thức - Formula iffOperator (Formula a1, Formula a2): phép “iff” giữa hai công thức - Formula impliesOperator (Formula a1, Formula a2): phép “implies” giữa hai công thức - Formula existsFomular (quant_var[] qv, Formula f): công thức được xây dựng với từ khóa “exists” - Formula forallFomular (quant_var[] qv, Formula f): công thức được xây dựng với từ khóa “forall” - Formula letFormula (varDecl var,Term t, Formula f): công thức được xây dựng với từ khóa “let” - Formula fletFormula (fvarDecl fvar,Formula f1, Formula f2): công thức được xây dựng với từ khóa “flet” 5.2.2.6. Lớp func_decl: khai báo một hàm của bài toán SMT, được xây dựng dựa trên (3) bảng 3. - func_decl (double d, Identifier id): khai báo một hàm từ giá trị một số thực và định danh Identifier Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 24 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng - func_decl (Identifier id1, Identifier[] id): khai báo một hàm từ giá trị một định danh Identifier và một mảng không rỗng định danh Identifier - func_decl (Arith_symb ar,Identifier[] id): khai báo một hàm từ một hoặc chuỗi các phép toán và mảng không rỗng các định danh id 5.2.2.7. Lớp pred_decl: khai báo một vị từ của bài toán SMT, được xây dựng dựa trên (4) bảng 3 - pred_decl (Identifier[] id): khai báo một vị từ với giá trị của một dịnh danh id - pred_decl (Arith_symb ar, Identifier[] id): khai báo một vị từ từ một (hoặc một chuỗi) các phép toán ar và một mảng các định danh id - pred_decl (Identifier id1, Identifier[] id): khai báo một vị từ từ một đinh danh id1 và mảng các định danh id 5.2.2.8. Lớp Term: được xây dựng dựa trên bảng 1. - Term (varDecl v): khái báo một term từ khai báo của một biến v - Term (double d): khai báo một term từ giá trị của một số thực d - Term (Identifier i): khai báo một term từ một đinh danh i - Term iteOperator (Formula f, Term t1, Term t2): toán tử “ite” của Term 5.2.2.9. Lớp annotation: được xây dựng dựa trên (15) bảng 1, dùng để khai báo một ghi chú trong bài toán SMT. Có hai cách khai báo như sau: - annotation (String attribute): khai báo ghi chú với chuỗi ký tự attribute - annotation (String attribute, String user_value): khai báo ghi chú với chuỗi ký tự thuộc tính attribute và user_value 5.2.2.10. Lớp varDecl: Dùng để khai báo một biến trong bài toán SMT. Được xây dựng dựa trên (8) bảng 1 - varDecl (String v): khai báo biến với chuỗi v 5.2.2.11. Lớp fvarDecl: được xây dựng dựa trên (9) bảng 1. - fvarDecl (String fv): dùng để khai báo fvar với chuỗi fv Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 25 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.2.2.12. Lớp Arith_symb: dùng để khai báo một hoặc một chuỗi các tự như đã được định nghĩa trong (10) bảng 1. - Arith_symb (String s): khai báo một hoặc 1 chuỗi các ký tự. 5.2.2.13. Lớp Identifier: được xây dựng dựa trên (7) bảng 1, để đưa ra các định danh cho bài toán SMT. - Identifier (String simpleIdentifier): khai báo định danh từ một định danh đơn giản (simple_identifier được định nghĩa trong (1) bảng 1) - Identifier (String simleID, long num): khai báo định danh từ một định danh đơn giản và một số nguyên) - Identifier (String simpleId,long num1, long[] num2): khai báo định danh từ một định danh đơn giản và một số nguyên cùng một mảng số nguyên. 5.2.2.14. Lớp quant_var: được xây dựng dựa trên (5) của bảng 2. - quant_var (varDecl var,Identifier id): khai báo quant_vả từ khai báo biến var và định danh id. Trên đây là các lớp và các hàm được xây dựng để hỗ trợ người dùng xây dựng bài toán SMT trước khi gửi lên máy chủ. Để xây dựng được một bài toán SMT đúng đắn bằng việc sử dụng các hàm trên, người dùng cần tuân thủ nghiêm ngặt các định nghĩa, cách khai báo các thành phần đã được đưa ra ở trên. Chương trình không hỗ trợ việc kiểm tra những gì người dùng nhập vào. Ví dụ với khai báo một đối tượng của lớp Arith_symb, người dùng buộc phải đưa vào một hoặc một chuỗi các ký tự thuộc tập các ký tự {=, >, <, &, @, #, +, -, *, /, %, |, ~ } Nếu người dùng đưa vào sai chuỗi được thiết lập từ các ký tự trên, tệp tin chứa bài toán SMT vẫn được sinh ra nhưng sẽ không đúng chuẩn và khi đó sẽ không có lời giải. Ngoài ra, do một số lớp có sử dụng đối tượng của lớp khác, nên người dùng cũng cần phải tuân thủ theo đúng việc khai báo các đối tượng của các lớp. Ví dụ, trước khi có được một đối tượng của lớp Bench_attribute, người dùng cần phải khai báo và xây dựng các đối tượng thuộc lớp Formula, annotation, funs_decl… Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 26 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.3. Phần máy trạm Chức năng của hệ thống được cài đặt trên máy trạm là nhận về bài toán SMT được máy chủ chuyển tới. Sau khi nhận được bài toán, hệ thống sẽ gọi chương trình để giải bài toán ấy. Sau khi có được lời giải của bài toán, hệ thống sẽ gửi lại phía máy chủ lởi giải đó. Trong trường hợp có máy trạm khác đã giải quyết xong bài toán ấy và gửi lên máy chủ trước khi chương trình giải được cài đặt trên hệ thống giải quyết xong bài toán, máy chủ sẽ gửi về một tín hiệu ngắt tiến trình đang chạy và không hệ thống sẽ dừng chương trình đang chạy và không gửi gì về phía máy chủ nữa. 5.3.1. Cơ chế làm việc của máy trạm Để đáp ứng nhu cầu nhận và giải liên tục các bài toán từ phía máy chủ, hệ thống máy trạm cần có cơ chế phù hợp để vừa có thể nhận liên tục dữ liệu từ máy chủ, vừa có thể thực thi việc giải bài toán (đã nhận xong từ phía máy chủ) và vừa có thể đảm bảo việc gửi lại chính xác kết quả của bài toán tương ứng sau khi đã giải xong. Để đáp ứng được yêu cầu này, hệ thống máy trạm cần được tổ chức các tác vụ thành các luồng tiến trình khác nhau. Trong ngôn ngữ lập trình Java, một luồng là một thuộc tính duy nhất [8] Nó là đơn vị nhỏ nhất của đoạn mã có thể thi hành được mà thực hiện một công việc riêng biệt. Một ứng dụng được viết bởi ngôn ngữ lập trình java có thể bao hàm nhiều luồng. Mỗi luồng được đăng ký một công việc riêng biệt, mà chúng được thực thi đồng thời với các luồng khác. Đa luồng giữ thời gian nhàn rỗi của hệ thống thành nhỏ nhất. Điều này cho phép các chương trình được viết bởi java có hiệu quả cao với sự tận dụng CPU là tối đa. Mỗi phần của chương trình được gọi một luồng, mỗi luồng định nghĩa một đường dẫn khác nhau của sự thực hiện. Việc phân luồng được ứng dụng trong hệ thống máy trạm sẽ được đề cập cụ thể hơn ở những phần sau của tài liệu. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 27 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.3.2. Quy định giao tiếp với máy chủ Do toàn bộ hệ thống được cài đặt trực tuyến, nên trường hợp nhận được nhiều bài toán tại một thời điểm là hoàn toàn có thể xảy ra. Để xác định đúng kết quả của bài toán tương ứng với bài toán nhận được trước đó, cần có một sự đánh dấu thứ tự cho các bài toán ấy. Nhóm nghiên cứu đã đưa ra và thống nhất sử dụng mã sessionID được tạo ra bởi máy chủ và được gửi kèm với nội dung. Việc sử dụng mã sessionID còn giúp hệ thống tránh được sự nhầm lẫn giữa hai hay nhiều bài toán cùng được gửi lên một lúc. Quy trình kết nối giữu máy trạm và máy chủ sẽ như sau: - Sau khi kết nối đến máy chủ, hệ thống cài đặt trên máy trạm sẽ gửi lời chào hỏi đến máy chủ thông qua thẻ cặp thẻ chào hỏi như sau: [Tên chương trình giải bài toán SMT] - Máy chủ sau khi nhận được lời chào sẽ gửi đến nội dung của bài toán SMT mà máy khách đã gửi lên yêu cầu giải. Việc gửi dữ liệu cũng được bắt đầu bằng thẻ mở và kèm thêm mã sessionID trước đó. Mỗi dòng dữ liệu của bài toán ấy gửi lên cũng sẽ kèm theo sessionID của bài toán đó cho đến khi thẻ đóng được gửi lên: sessionID | sessionID | [nội dung dòng dữ liệu thứ 1] …. sessionID | [nội dung dòng dữ liệu thứ n] sessionID | - Sauk hi nhận được dữ liệu từ tệp tin chứa bài toán SMT, hệ thống sẽ nhận trễ thời gian giới hạn thực thi bài toán ấy. Việc nhận trễ thời gian giới hạn này được quy định như sau: sessionID | sessionID | [trễ thời gian] sessionID | Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 28 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng - Sau khi đã có dữ liệu đầy đủ của một bài toán hệt thống sẽ gọi chương trình giải bài toán SMT để thực hiện việc giải bài toán đó. Sau khi có kết quả, hệ thống sẽ gửi lại máy chủ theo quy chuẩn sau: sessionID | sessionID | [nội dung dòng kết quả trả về thứ 1] ….. sessionID | [nội dung dòng kết quả trả về thứ 2] sessionID | - Sau khi gửi về kết quả, hệ thống sẽ vẫn tiếp tục nhận hoặc chờ bài toán tiếp theo mà máy chủ sẽ gửi đến. 5.3.3. Hoạt động của hệ thống máy trạm Với mỗi bài toán, hệ thống sẽ ghi vào một tệp tin có tên chính là sessionID của bài toán ấy với phần mở rộng là smt. Và lời giải của bài toán đó cũng sẽ được lưu trữ vào tệp tin có tên là sessionID. Hiện tại, trên thế giới có nhiều các bộ giải bài toán SMT, tuy nhiên, trong khuôn khổ luận văn này, hệ thống chỉ cài đặt và thử nghiệm trên hai bộ giải là yices của SRI international và Z3 của Microsoft. Mỗi bộ giải sẽ được cài đặt trên một máy trạm khác nhau cùng với hệ thống được xây dựng như đã trình bày ở trên. Do các bộ giải là các chương trình chạy độc lập, nên hệ thống cần có lời gọi thực thi tới chúng. Tuy ngôn ngữ lập trình Java có hỗ trợ việc gọi một lệnh của hệ điều hành, tuy nhiên để có thể kết xuất được kết quả ra một tệp tin, hệ thống sử dụng quá trình chuyển hướng kết xuất của chính hệ điều hành được sử dụng. Do điệu kiện không cho phép, hiện tại hệ thống cài đặt trên máy trạm mới chỉ được triển khai và kiểm thử trên các máy sử dụng hề điều hành windows và hệ hiều hành có nhân Linux. Và để sử dụng được chuyển hướng kết xuất trên mỗi hệ điều hành khác nhau, hệ thống đã xây dựng một tệp tin thực thi để hỗ trợ hệ thống gọi các bộ giải SMT. Nội dung tệp tin hỗ trợ đó như sau: - Đối với tệp tin .bat được cài đặt trên hệ điều hành windows @echo off [path]\yices.exe -e -tm %2 -smt [path]\%1.smt > [path]\%1.txt echo done! Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 29 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng - Đối với tệp tin thực thi (tệp tin được thiết lập thuộc tính thực thi) được cài đặt trên hệ điều hành Linux: [path]/z3.exe /m /t:$2 /smt [path]/$1.smt > [path]/$1.txt echo done! - Ở đây, [path] là đường dẫn chỉ đến tệp tin (thư mục) của chương trình bộ giải SMT. %1 sẽ được nhận vào là sesstionID của bài toán. %2 sẽ là tham số thời gian ngắt của chương trình (được tính bằng giây). - Với bộ giải yices, ta sử dụng tham số -e để đưa ra kết quả thỏa mãn nếu bài toán đó khả thi. Tham số –tm để xác định trễ thời gian ngắt timeout, và tham số -smt để xác định đầu vào của bộ giải là một tệp tin theo chuẩn SMT-LIB. - Với bộ giải z3, tương tự ta cũng có các tham số /m tương đương với –e, /t: tương đương với –tm và /smt tương đương với –smt của bộ giải yices. - Cả hai bộ giải yices và z3 đều hỗ trợ cài đặt trên cả windows và Linux, vì vậy, tùy vào điệu kiện của máy trạm, tệp tin thực thi sẽ được sửa cho phù hợp với hệ điều hành cài đặt (không nhất thiết cài đặt yices trên hệ điều hành windows hoặc z3 trên linux). Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.3.4. Các lớp của hệ thống máy trạm 5.3.4.1. Biểu đồ lớp của hệ thống Hình 5.1: Biểu đồ lớp của hệ thống máy trạm 5.3.4.2. Lớp config Lớp config chứa những quy định về địa chỉ, cổng và các thẻ giao tiếp với máy chủ của máy trạm. Ngoài ra, lớp này còn quy định tên và đường dẫn của bộ giải được cài đặt trên máy trạm. Việc xây dựng lớp config sẽ khiến cho việc quản lý cấu hình cho hệ thống dễ dàng hơn. 5.3.4.3. Lớp sessionID Để xác định được đúng dữ liệu của mỗi bài toán, tránh nhầm lẫn khi nhận nhiều dòng dữ liệu từ nhiều bài toán cùng một lúc, và để gửi đúng lời giải cho bài toán đưa ra, ngoài việc quy định mã sessionID cho mỗi bài toán, cần phải tổ chức dữ liệu hợp lý. Đối với kết quả của một bài toán được gửi đến, ta chỉ cần đưa kết quả đó vào một Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 31 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng tệp tin với trên tệp tin là sessionID của bài toán đó, rồi gửi lại máy chủ session ID kèm nội dung tệp tin đó. Còn đối với việc đọc dữ liệu đầu vào, hệ thống xây dựng một lớp sessionID và có một mảng đối tượng của lớp dữ liệu này. Lớp session ID sẽ bao gồm các thuộc tính sau: - sessionID: là thuộc tính lưu lại sessionID - content: Thuộc tính lưu lại nội dung của bài toán tương ứng với sessionID được gửi lên. - Timeout: thời gian ngắt của bài toán được gửi lên - runSolver: tiến trình gọi một bộ giải để giải bài toán được gửi lên. Mỗi đối tượng của lớp sessionID sẽ tương ứng với một bài toán được gửi lên. Nội dung của bài toán sẽ được lưu trong thuộc tính content của lớp. Mỗi tiến trình xử lý sẽ được khai báo bởi thuộc tính runSolver của lớp. Việc đưa tiến trình xử lý gọi bộ giải để giải bài toán vào thành thuộc tính của lớp sessionID nhằm giải quyết vấn đề ngắt tiến trình khi có yêu cầu từ phía máy chủ. Khi máy chủ nhận được kết quả của cùng bài toán từ máy trạm có cài đặt bộ giải khác và gửi lên tín hiệu ngắt cho máy trạm đang còn thực thi tiến trình giải bài toán ấy, thì việc ngắt tiến trình tương ứng với sessionID mà máy chủ gửi lên sẽ được gọi. 5.3.4.4. Lớp Solver Lớp này được xây dựng để thực hiện nhiệm vụ mở kết nối và có lời chào hỏi trước khi thực hiện các thao tác khác sau đó. 5.3.4.5. Lớp ReadThread Lớp này được xây dựng để đáp ứng việc đọc dữ liệu từ máy chủ gửi lên của máy trạm. Sau khi kết nối được giữa máy chủ và máy trạm, hệ thống trên máy trạm luôn đảm bảo việc lắng nghe các tín hiệu từ máy chủ. Để đảm bảo rằng, luôn có thể nhận được nhiều dòng dữ liệu từ nhiều các bài toán khác nhau cùng một lúc. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 32 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Vấn đề kiểm soát bộ nhớ (mảng các đối tượng sessionID) sẽ được đánh dấu bằng việc bài toán đã được giải xong hay chưa. Khi một sessionID mới được nhận về, một phần tử của mảng các đối tượng sessionID mà có trạng thái rảnh sẽ được khởi tạo và lưu lại. khi đó, trạng thái tương ứng của sessionID được bật là bận. Do việc giải phóng bộ nhớ phụ thuộc vào việc bài toán được giải xong hay chưa, vì vậy trạng thái của sessionID được khai báo trong lớp các đối tượng tiến trình ghi dữ liệu. Tức là tương ứng với mảng các đối tượng của lớp sesstionID, sẽ có một mảng các đối tượng ghi dữ liệu kết quả trả về được khởi tạo. while (true){ _return = in.readLine(); //Đọc dữ liệu gửi lên từ phía máy chủ if (_return.indexOf(config._tag_file)>=0){ openFile(_return); // Tạo mới một tệp tin lưu trữ bài toán mới } else if(_return.indexOf(config._closetag_file)>=0){ } else if(_return.indexOf(config._tag_timeout)>=0){ sec[k].setTimeout(_return.substring(p+1));//đặt trễ thời gian cho bài toán closeFile(_return); // } else if(_return.indexOf(config._tag_destroy)>=0){ k = pos(_return); // xác định bài toán cần ngắt interruptSolver(k); // Ngắt tiến trình xử lý bài toán } else { k = pos(_return); String content = _return.substring(p+1); sec[k].content += content + "\n"; //lưu lại nội dung bài toán } } Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 33 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Ngay khi tiếp nhận một bài toán mới (nhận được thẻ mở tệp tin), đối tượng của lớp ghi dữ liệu tương ứng sẽ được đặt thuộc tính là bận. Việc quản lý thiết lập thuộc tính bận hay rảnh này sẽ giúp cho hệ thống giới hạn được số lượng phần tử mảng luồng đọc ghi dữ liệu. Trong trường hợp không quản lý trạng thái rảnh hay bận của các đối tượng này, mỗi khi nhận được bài toán mới, hệ thống sẽ sinh ra một phần tử của mảng các đối tượng ghi dữ liệu. Như vậy, các đối tượng ghi xong và được giải phóng sẽ không được sử dụng lại, gây ra lãng phí tài nguyên. Việc gọi tiến trình thực thi các bộ giải sẽ được thực hiện khi việc nhận dữ liệu về bài toán được hoàn tất. Sau khi nhận được tham số trễ thời gian, hệ thống sẽ tiến hành ghi dữ liệu ra tệp tin và gọi lệnh gọi bộ giải để giải quyết bài toán. Và khi đó, tiến trình này sẽ được truyền cho đối tượng của lớp ghi dữ liệu để nhận và trả về kết quả. String command = config._command + " " + sec[k].sectionID + " " + sec[k].getTimeout(); sec[k].runSolver = Runtime.getRuntime().exec(command); wt[k].setProc(sec[k].runSolver); public ReadThread(Socket sk){ try { for (int i = 0;i<config.Max_connection;i++) { sec[i] = new section(); //khởi tạo mảng các đối tượng sessionID wt[i] = new WriteThread(sk); //Khởi tạo mảng các đối tượng ghi dữ liệu } } catch (IOException e){ e.printStackTrace(); } } Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 34 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 5.3.4.6. Lớp WriteThread Việc chờ kết quả để gửi trả về phía máy chủ cần được xây dựng thành một luồng làm việc riêng biệt bởi đi kèm với việc gửi trả về kết quả, là việc trả về không gian bộ nhớ cho thành phần đối tượng thuộc lớp sessionID. Ngoài ra, luồng này còn luôn sẵn sàng để ngắt tiến trình đang thực hiện nếu có yêu cầu từ phía máy chủ gửi lên. Ngoài ra, tính cần thiết phải đưa thành một luồng làm việc riêng biệt còn thể hiện ở việc đáp ứng yêu cầu luôn lắng nghe dữ liệu gửi lên từ phía máy chủ. Đối với việc gọi và thực thi bộ giải, sau khi dữ liệu được ghi vào tệp tin hoàn tất, một tiến trình (thành phần của lớp sessionID) sẽ gọi công cụ giải được cài đặt trên máy trạm. Khi nhận được tín hiệu “done!” xuất hiện từ luồng dữ liệu ra của tiến trình, bài toán đã được giải xong và quá trình gửi dữ liệu về máy chủ được bắt đầu. Cùng với đó, bộ nhớ chứa dữ liệu của bài toán được thực thi xong sẽ được giải phóng. Việc ngắt một tiến trình khi nhận được yêu cầu ngắt từ phía máy chủ cũng được đẩy sang phương thức của lớp này. Bởi lẽ, việc ngắt tiến trình còn liên quan đến việc thiết lập trạng thái rảnh cho đối tượng. 5.4. Tổng kết Mỗi hệ thống con của hệ thống giải bài toán SMT hiệu năng cao mang vai trò riêng và đều rất quan trọng với hệ thống. Việc xây dựng tốt hệ thống máy khách sẽ public void interruptSolver(){ this.proc.destroy(); //ngắt tiến trình đang xử lý this.active = false; // trả về trạng thái rảnh } if (line.equals("done!")){ sendFile(); // gửi tệp tin kết quả this.active = false; // thiết lập trạng thái rảnh cho đối tượng this.stop(); } Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 35 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng giúp người dùng thuận tiện hơn nhiều trong quá trình xây dựng bài toán SMT. Còn đối với hệ thống máy trạm, nếu được xây dựng tốt sẽ giúp cho hiệu năng xử lý bài toán SMT sẽ tăng cao, giúp cho hiệu năng toàn hệ thống được cải thiện. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 36 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Chương 6. Cài đặt và thử nghiệm 6.1. Cài đặt Đối với hệ thống máy khách, việc cài đặt sẽ phụ thuộc vào người sử dụng. Do hệ thống được xây dựng như một thư viện người dùng, nên việc đưa vào những đoạn mã chương trình của người dùng là rất dễ dàng. Hệ thống cũng hỗ trợ người dùng thực thi trực tiếp nếu đã có tệp tin chứa nội dung bài toán SMT theo đúng chuẩn của SMT- LIB Đối với hệ thống máy khách. Java là một ngôn ngữ không phụ thuộc vào hệ điều hành khi biên dịch nên hệ thống có thể cài đặt trên mọi hệ điều hành khác nhau. Tuy nhiên, do hệ thống có sử dụng việc gọi tiến trình và kết xuất dữ liệu, nên việc cài đặt trên hệ điều hành khác nhau cần có sự tùy chỉnh về mã lệnh cũng như tệp tin hỗ trợ. Trong phần thử nghiệm của nhóm phát triển, hệ thống máy khách được cài đặt trên mộ máy tính có cấu hình phổ biến hiện nay và sử dụng nền hệ điều hành windows. Phần máy trạm sẽ được cài đặt song song hai bộ giải trên hai máy khác nhau: Một máy có nền windows 7 và một máy được cài sẵn hệ điều hành Linux CenOS. 6.2. Bài toán thực nghiệm Bài toán thực nghiệm được xây dựng nhằm kiểm tra tính đúng đắn cũng như hiệu năng sử dụng của hệ thống. 6.2.1. Xây dựng bài toán SMT dựa trên các hàm API Từ những hàm API của hệ thống được cài đặt trên máy khách, ta xây dựng một chương trình sử dụng các hàm API đó để xây dựng một bài toán SMT hoàn chỉnh. Việc sử dụng các hàm API được tuân thủ chặt chẽ theo luật và định nghĩa đã được nêu trong phần kiến thức nền tảng và phần hướng đẫn các hàm API. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 37 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng 6.2.2. Thử nghiệm kết nối với máy chủ và toàn hệ thống Để thử nghiệm hoạt động của toàn hệ thống, nhóm phát triển đã sử dụng một số các tệp tin được xây dựng và đưa ra của SMT-LIB. Cụ thể Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm Tên tệp tin Kích thước Logic Trạng thái Test1.SMT 1kb QF_UF sat Test2.SMT 3kb QF_AX sat Test3.SMT 1kb QF_AUFLIA sat Test4.SMT 312kb QF_LIA sat Test5.SMT 587kb QF_LIA unsat Test6.SMT 270kb QF_LRA sat Với tất cả các file dữ liệu kiểm thử được sử dụng như trên, ta tùy chỉnh để hệ thống có thể chạy tối đa 6 kết nối cùng một lúc, số lượng kết nối chờ là 500. Hệ thống cho thấy được khả năng đáp ứng tốt tất cả các yêu cầu của người dùng, đáp ứng kết quả chính xác và thời gian đáp ứng nhanh chóng, hệ thống đưa về kết quả nhanh nhất trong các bộ giải. Dựa vào những file dữ liệu để kiểm thử hệ thống như trên, ta có kết quả của hệ thống về mặt thời gian như sau: Bảng 9: Kết quả thời gian của thực nghiệm Solver Tên file Z3 Yieces All Test1.smt 1 1 1 Test2.smt 1 1 1 Test3.smt 1 1 1 Test4.smt 7 8 7 Test5.smt 20 16 16 Test6.smt 35 35 35 Kết quả trả về đối với từng bộ giải: Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 38 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Bảng 10: Kêt quả trả về của thực nghiệm Solver Tên file Z3 Yieces All Test1.smt Sat Sat Sat Test2.smt Sat Error Sat Test3.smt Sat Sat Sat Test4.smt Sat Sat Sat Test5.smt Unsat Unsat Unsat Test6.smt Time out TimeOut TimeOut Từ kết hai bảng kết quả trên, ta có thể thấy rằng, hiệu quả đem lại của hệ thống giải bài toán SMT là khá rõ ràng. Với những bài toán lớn, rõ ràng thời gian trả về của các bộ giải là rất quan trọng. Tuy nhiên, với việc kết hợp nhiều bộ giải, vấn đề tối ưu hóa thời gian giải bài toán đã được giải quyết. Qua những ví dụ 4, 5 ta thấy rằng thời gian giải của các bộ giải đã có sự chênh lệch, và hệ thống đã đưa ra được thời gian trả về kết quả tối ưu nhất. Từ bảng 10, ta có thể thấy rằng, hầu hết các ví dụ đều có kết quả giống nhau. Tuy nhiên, trong trường hợp kết quả trả về khác nhau, hệ thống vẫn đưa ra được kết quả đúng đắn nhất cho người sử dụng. Ta thấy rằng, ở ví dụ 2, bộ giải yices đã không thể đưa ra được kết quả (vì không hỗ trợ logic này), tuy nhiên bộ giải Z3 vẫn đưa ra được kết quả cho bài toán. Còn ở ví dụ 6, ta thấy rằng, hệ thống đã hoạt động tốt với chức năng thiết lập thời gian chờ tối đa của người dùng. Hệ thống đã ngắt và trả về cho người sử dụng trạng thái của bài toán mà người dùng gửi lên. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 39 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Kết Luận Với hệ thống giải quyết bài toán SMT hiệu năng cao đã được xây dựng và trình bày ở trên, việc giải quyết các bài toán SMT sẽ dễ dàng và mang lại nhiều hiệu quả hơn rất nhiều cho người sử dụng. Tuy rằng, hệ thống mới chỉ được nghiên cứu và phát triển trong những bước đầu hết sức đơn giản, nhưng những hiệu quả mang lại đã được chứng minh rất rõ ràng trong phần thực nghiệm hệ thống. Do sử dụng nhiều bộ giải cùng một lúc với cùng một bài toán nên ngoài khả năng tối ưu hóa mặt thời gian, hệ thống còn có thể tối ưu hóa khả năng giải quyết bài toán SMT dưới nhiều chuẩn Logic, nền lý thuyết khác nhau. Với việc xây dựng hệ thống máy khách và máy trạm, cá nhân tôi đã có được những hiểu biết nhất định về cấu trúc bài toán SMT cũng như việc phân luồng các tiến trình để tận dụng được tối đa hiệu năng của máy. Tuy những hiểu biết và thành quả còn nhiều hạn chế, nhưng đây là bước đầu để có thể phát triển hoàn thiện hệ thống giải bài toán SMT hiệu năng cao về sau. Việc nghiên cứu và phát triển hệ thống giải quyết tối ưu bài toán SMT một cách đầy đủ, hoàn thiện hơn cần sự đầu tư về thời gian, trí óc và nhân sự. Rất mong sẽ có những người cùng phát triển hệ thống về sau để hình thành nên hệ thống giải quyết bài toán SMT tốt hơn. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 40 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Hướng phát triển tiếp theo của hệ thống Tuy hệ thống giải quyết bài toán SMT hiệu năng cao có những thành quả rất khả quan, nhưng vẫn còn nhiều các hạn chế cần phải đầu tư và phát triển. Đối với toàn hệ thống, hiện tại hệ thống chỉ hỗ trợ các bài toán thuộc chuẩn của SMT-LIB trong khi đó, các bộ giải đều hỗ trợ những chuẩn đầu vào riêng. Vì vậy hệ thống cần phải phát triển để có thể đáp ứng được nhiều các chuẩn đầu vào khác nữa để giải quyết. Hướng giải quyết cho vấn đề này sẽ có hai cách thức: thứ nhất, hệ thống sẽ xây dựng một bộ chuyển tất cả các đầu vào thành dạng chung SMT-LIB rồi phần bổ cho các máy trạm xử lý, hoặc cách thứ hai có thể tìm và đưa cho đúng bộ giải hỗ trợ loại định dạng đầu vào đó để xử lý. Về phía máy khách, hiện tại hệ thống cài đặt trên máy khách chỉ hỗ trợ việc xây dựng bài toán SMT hoàn toàn phải dựa trên định nghĩa và luật ngữ nghĩa được ghi trong các bảng (1), (2), (3), (4), (5). Điều này khiến cho người dụng gặp nhiều khó khăn khi buộc phải nhớ các luật ngữ nghĩa đó. Vì vậy, hệ thống cài đặt trên máy khách cần xây dựng những hàm nhúng API đơn giản, hiệu quả và dễ dàng sử dụng hơn đối với người dùng. Ngoài ra, hệ thống nên có một giao diện trực quan khi người dùng chỉ sử dụng chức năng chỉ ra tập tin chứa bài toán SMT cần giải quyết. Về phía máy trạm, do khuôn khổ luận văn có hạn, nên hiện tại hệ thống mới chỉ sử dụng được hai bộ giải là yices và Z3, điều này khiến hệ thống sẽ có nhiều hạn chế về hiệu năng xử lý các bài toán SMT được đưa vào. Vì vậy, hệ thống cần được nghiên cứu, phát triển để có thể sử dụng nhiều hơn các bộ giải khác vào việc xử lý song song các bài toán SMT. Ngoài ra, hệ thống cần phải nghiên cứu và phát triển trên nhiều nền hệ điều hành khác nhau nữa. Hiện tại, việc gọi các bộ giải còn cần phải thông qua một tệp tin thực thi của hệ điều hành, nên việc cài đặt hệ thống còn đang bị giới hạn trên hai hệ điều hành là windows và linux. Xây dựng hệ thống giải bài toán SMT hiệu năng cao – Phần máy trạm 2010 Trang 41 Sinh viên: Hoàng Thế Tùng – K51CNPM – Khoa CNTT - ĐH Công nghệ - ĐH QGHN GVHD: TS. Trương Anh Hoàng GVĐHD: TS. Phạm Ngọc Hùng Tài liệu tham khảo [1] Roberto Sebastiani, Sanjit A. Seshia and Cesare Tinelli Clark Barrett, "Satisfiability Modulo Theories," in Handbook of Satisfiability., 2008, ch. 12, p. 737. [2] Leonardo de Moura and Nikolaj Bjorner, Satisfiability Modulo Theories: An Appetizer. WA: Microsoft Research. [3] N. Shankar, A Tutorial on Satisfiability Modulo Theories. CA: Computer Science Laboratory. [4] Silvio Ranise, Cesare Tinelli, The SMT-LIB Format: An Initial Proposal., 2006. [5] Bruno Dutertre and Leonardo de Moura, The YICES SMT Solver.: Computer Science Laboratory, SRI International. [6] Aaron Stump, and Cesare Tinelli Clark Barrett. (2006) www.SMT-LIB.org. [7] Silvio Ranise, Cesare Tinelli, The SMT-LIB Standard: Version 1.2., 2006. [8] Cay S Horstmann and Gary Cornell, Core Java.: Pearson Education, 2008.