Khóa luậ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

ĐẠI HỌC QUỐC GIA HÀ NỘI TRƯỜNG ĐẠI HỌC CÔNG NGHỆ Hoàng Thế Tùng 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 KHOÁ LUẬN TỐT NGHIỆP ĐẠI HỌC HỆ CHÍNH QUY Ngành: Công nghệ phần mềm Cán bộ hướng dẫn: TS. Trương Anh Hoàng Cán bộ đồng hướng dẫn: TS. Phạm Ngọc Hùng HÀ NỘI - 2010 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 Lời cảm ơn Trước hết, tôi xin gửi lời cảm ơn chân thành và sâu sắc đến Tiến sỹ Trương Anh Hoàng và Tiến sỹ Phạm Ngọc Hùng, những người đã trực tiếp hướng dẫn tôi trong suốt quá trình nghiên cứu và phát triển đề tài nghiên cứu này. Để có được những kết quả nghiên cứu như hiện nay, tôi vô cùng biết ơn sự quan tâm, hướng dẫn nhiệt tình của hai thầy trong thời gian vừa qua. Tôi xin chân thành cảm ơn các thầy cô trong trường Đại học công nghệ, Đại học Quốc Gia Hà Nội nói chung, và các thầy cô trong khoa công nghệ thông tin nói riêng, những người đã nhiệt tình giảng dạy, giúp tôi có những kiến thức quý báu để tôi có thể hoàn thành được đề tài luận văn này. Tôi xin bày tỏ lòng cảm ơn đến các anh chị cao học, và các bạn trong nhóm nghiên cứu đã cùng tôi tìm hiểu và xây dựng hoàn chỉnh hệ thống giải quyết bài toán Satisfiability Modulo Theories (SMT) với hiệu năng cao, giúp tôi có thể hoàn thành tốt phần nghiên cứu của mình. Và cuối cùng, tôi xin gửi lời cảm ơn đến gia đình, bạn bè và những người thân đã bên cạnh, động viên giúp tôi hoàn thành tốt luận văn của mình. Hà Nội, tháng 05/2010 Hoàng Thế Tùng 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 Tóm tắt nội dung Vấn đề giải quyết các bài toán Satisfiability Modulo Theories (SMT) hiện nay đang được nghiên cứu và phát triển ở nhiều nơi trên thế giới. Cho đến ngày nay, nhiều trường đại học, tổ chức đã nghiên cứu và đưa ra những bộ giải giải quyết bài toán SMT (hay còn gọi là SMT solver). Ví dụ như Z3 của Mcrosoft, yices của SRI, CVC3 của một số trường đại học danh tiếng của Mỹ. hay boolector, openSMT của một số trường đại học danh tiếng khác… Tuy nhiên, mỗi solver có một lợi thế ưu điểm riêng đối với các dạng khác nhau của bài toán SMT. Vậy vấn đề đặt ra là làm sao để tận dụng được hết các ưu điểm đó cho từng bài toán. Để giải quyết vấn đề ấy, nhóm nghiên cứu đã nghiên cứu và xây dựng một hệ thống giải quyết bài toán SMT trực tuyến, kết hợp nhiều bộ giải khác nhau để đưa ra được lời giải tối ưu cho từng bài toán SMT. Trong khuôn khổ khóa luận tốt nghiệp này của cá nhân tôi, tôi đã xây dựng hai hệ thống con của hệ thống đã nêu trên là hệ thống trên máy khách (users) và trên máy trạm (sử dụng để gọi các Solver). Hệ thống trên máy khách sẽ đảm nhiệm việc cung cấp một giao diện lập trình ứng dụng (Application Programming Interface hay API) để người dùng sử dụng có thể xây dựng bài toán SMT theo chuẩn thư viện SMT (SMT- LIB) và sau đó là gửi bài toán đến máy chủ (server). Hệ thống trên máy trạm sẽ tiếp nhận bài toán từ máy chủ và gọi các bộ giải để giải quyết bài toán đó và gửi về máy chủ kết quả. 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 Mục lục Chương 1. Mở đầu .................................................................................................................. 1 1.1. Giới thiệu ..................................................................................................................... 1 1.2. Bài toán đặt ra .............................................................................................................. 1 1.3. Cấu trúc nội dung tài liệu ............................................................................................. 2 Chương 2. Kiến thức nền tảng ................................................................................................ 3 2.1. Giới thiệu SMT ............................................................................................................ 3 2.2. Bộ giải SMT (SMT solver) .......................................................................................... 3 2.3. Thư viện SMT (SMT-LIB) .......................................................................................... 4 2.3.1. Cấu trúc cơ bản của SMT-LIB ............................................................................. 4 2.3.2. Khuôn dạng của SMT-LIB ................................................................................... 5 Chương 3. Phân tích hệ thống .............................................................................................. 12 3.1. Mô hình hệ thống ....................................................................................................... 12 3.2. Mô hình ca sử dụng của hệ thống .............................................................................. 13 3.3. Mô hình hoạt động ..................................................................................................... 15 Chương 4. Phương hướng giải quyết vấn đề ........................................................................ 17 4.1. Lựa chọn phương thức kết nối ................................................................................... 17 4.2. Lựa chọn ngôn ngữ lập trình ...................................................................................... 17 4.3. Xác định dữ liệu đầu vào, đầu ra của hệ thống .......................................................... 17 Chương 5. Mô tả hệ thống .................................................................................................... 19 5.1. Quy định cách thức giao tiếp với máy chủ ................................................................ 19 5.2. Phần máy khách ......................................................................................................... 20 5.2.1. Quy định giao tiếp với máy chủ ......................................................................... 20 5.2.2. Các lớp của hệ thống máy khách ........................................................................ 21 5.2.2.1. Lớp config ................................................................................................... 21 5.2.2.2. Lớp Client: .................................................................................................. 21 5.2.2.3. Lớp NetSolver ............................................................................................. 21 5.2.2.4. Lớp Bench_attribute .................................................................................... 22 5.2.2.5. Lớp Formula ................................................................................................ 22 5.2.2.6. Lớp func_decl .............................................................................................. 23 5.2.2.7. Lớp pred_decl .............................................................................................. 24 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.2.2.8. Lớp Term ..................................................................................................... 24 5.2.2.9. Lớp annotation ............................................................................................ 24 5.2.2.10. Lớp varDecl ................................................................................................ 24 5.2.2.11. Lớp fvarDecl ............................................................................................... 24 5.2.2.12. Lớp Arith_symb .......................................................................................... 25 5.2.2.13. Lớp Identifier .............................................................................................. 25 5.2.2.14. Lớp quant_var ............................................................................................. 25 5.3. Phần máy trạm ........................................................................................................... 26 5.3.1. Cơ chế làm việc của máy trạm ........................................................................... 26 5.3.2. Quy định giao tiếp với máy chủ ......................................................................... 27 5.3.3. Hoạt động của hệ thống máy trạm ...................................................................... 28 5.3.4. Các lớp của hệ thống máy trạm .......................................................................... 30 5.3.4.1. Biểu đồ lớp của hệ thống ............................................................................. 30 5.3.4.2. Lớp config ................................................................................................... 30 5.3.4.3. Lớp sessionID .............................................................................................. 30 5.3.4.4. Lớp Solver ................................................................................................... 31 5.3.4.5. Lớp ReadThread .......................................................................................... 31 5.3.4.6. Lớp WriteThread ......................................................................................... 34 5.4. Tổng kết ..................................................................................................................... 34 Chương 6. Cài đặt và thử nghiệm ......................................................................................... 36 6.1. Cài đặt ........................................................................................................................ 36 6.2. Bài toán thực nghiệm ................................................................................................. 36 6.2.1. Xây dựng bài toán SMT dựa trên các hàm API.................................................. 36 6.2.2. Thử nghiệm kết nối với máy chủ và toàn hệ thống ............................................ 37 Hướng phát triển tiếp theo của hệ thống .............................................................................. 40 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 Danh sách các bảng trong tài liệu Bảng 1: Luật sinh một toán hạng ................................................................................................ 7 Bảng 2: Luật sinh một công thức ................................................................................................ 8 Bảng 3: Luật sinh một thuyết ..................................................................................................... 8 Bảng 4: Luật sinh một logic ....................................................................................................... 8 Bảng 5 Luật sinh một chuẩn ....................................................................................................... 9 Bảng 6: Các lý thuyết nền được quy chuẩn trong SMT-LIB 1.2 ............................................... 9 Bảng 7: Các Logic quy chuẩn được đưa ra trong SMT-LIB 1.2 .............................................. 10 Bảng 8 Bảng dữ liệu các tệp tin đầu vào thử nghiệm ............................................................... 37 Bảng 9: Kết quả thời gian của thực nghiệm ............................................................................. 37 Bảng 10: Kêt quả trả về của thực nghiệm ................................................................................ 38 Danh sách các hình trong tài liệu Hình 3.1 Mô hình hệ thống giải bài toán SMT hiệu năng cao. ............................................... 12 Hình 3.2: Mô hình ca sử dụng của hệ thống ............................................................................ 14 Hình 3.3: Mô hình hoạt động của hệ thống ............................................................................. 15 Hình 5.1: Biểu đồ lớp của hệ thống máy trạm ......................................................................... 30 Danh sách từ viết tắt trong tài liệu Từ viết tắt Từ chuẩn Diễn giải SMT Satisfiability Modulo Theories Các lý thuyết module về tính thỏa được SMT-LIB Satisfiability Modulo Theories - Liblary Thư viện các lý thuyết module về tính thỏa được API Application Programming Interface Giao diện lập trình ứng dụng 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 1 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 1. Mở đầu 1.1. Giới thiệu Hiện nay, cùng với sự phát triển bùng nổ của hầu hết các ngành khoa học, ngành khoa học máy tính cũng có những tiến bộ to lớn. Song song với đó, nhu cần nghiên cứu về việc giải hoặc đưa ra tính khả thi của một biểu thức logic ngày càng được quan tâm và phát triển. Bởi lẽ, rất nhiều các ứng dụng hay những sự tính toán trong ngành khoa học máy tính cần đến những công thức logic phức tạp. Trong khoảng hai thập niên gần đây, ngành khoa học máy tính đã có những tiến bộ lớn đối với việc tự động chứng minh hay bác bỏ tính đúng đắn của một biểu thức logic. Tuy nhiên việc chứng minh các biểu thức logic sẽ khó khăn hơn nhiều nếu đặt chúng trong một nền lý thuyết thay vì chứng minh một cách tổng quát [1,2]. Những vấn đề này được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories hay còn được viết tắt là SMT [1]). Cho đến nay, nhiều trường đại học cùng những nhà nghiên cứu khoa học máy tính đã có những nghiên cứu, sản phẩm để giải quyết vấn đề này. Tuy nhiên, việc xây dựng một bộ giải các vấn đề SMT tối ưu cho mọi trường hợp và rất khó khăn. Vì vậy, vấn đề được đặt ra là kết hợp các bộ giải SMT đó để có được một bộ giải tối ưu nhất về mặt thời gian. 1.2. Bài toán đặt ra Đối với việc giải quyết các vấn đề SMT, nhiều trường đại học cũng như các cơ quan, tổ chức lớn trên thế giới đã có những nghiên cứu và đưa ra những sản phẩm của mình. Tuy nhiên, với mỗi sản phẩm, họ đưa vào những thuật toán khác nhau để giải quyết vấn đề này. Trong khuôn khổ đồ án, việc nghiên cứu cơ chế, và tính đúng đắn của những bộ giải này không được đề cập đến (kết quả đưa ra của các bộ giải sẽ được coi là luôn đúng đắn) mà sẽ tập trung vào việc sử dụng những bộ giải này như là những công cụ giải quyết vấn đề SMT được đưa vào. Với những kết quả đưa ra bởi các bộ giải này, cần có một kết trả được trả về tối ưu nhất về mặt thời gian. 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 2 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ải quyết vấn đề nói trên, cần có một hệ thống phân phối các vấn đề SMT cho các bộ giải và nhận về kết quả trả về tối ưu nhất về mặt thời gian. Ngoài ra để tiện cho việc sử dụng và phát triển hệ thống, cần có một thư viện các hàm nhúng hỗ trợ người sử dụng xây dựng các vấn đề SMT. 1.3. Cấu trúc nội dung tài liệu Tài liệu này nhằm giới thiệu về bài toán SMT và mô tả hệ thống giải quyết bài toán đó trực tuyến. Chương mở đầu của tài liệu giới thiệu qua về bài toán SMT và bài toán đặt ra cho việc xây dựng hệ thống giải quyết bài toán SMT đó. Chương thứ hai của tài liệu đề cập tới một số kiến thức về SMT và cấu trúc, khuôn dạng của bài toán SMT được xây dựng theo chuẩn SMT-LIB. Chương này được coi là kiến thức nền tảng để xây dựng hệ thống giải quyết bài toán SMT hiệu năng cao. Những kiến thức trong chương này sẽ được sử dụng để xây dựng các hàm API cho hệ thống máy khách và một số thành phần của hệ thống máy trạm. Chương ba và chương bốn là phần phân tích và hướng giải quyết vấn đề xây dựng hệ thống giải bài toán SMT hiệu năng cao. Chương ba sẽ tập trung hơn vào vấn đề phân tích, đưa ra một cái nhìn tổng quan về hệ thống và quy trình hệ thống sẽ hoạt động. Chương bốn sẽ là một số lựa chọn giải pháp để giải quyết một số vấn đề khi xây dựng hệ thống. Hệ thống giải bài toán SMT hiệu năng cao phần máy trạm và máy khách sẽ được mô tả chi tiết trong chương năm. Ở chương này, hệ thống các hàm API trên máy khách sẽ được mô tả rất chi tiết và có thể coi là tài liệu hướng dẫn cho người dùng sử dụng các hàm API này. Chương sáu sẽ đưa ra phần thực nghiệm và đánh giá kết quả của hệ thống. Trong chương này, kết quả của một số thực nghiệm hệ thống sẽ được đưa ra nhằm đưa ra một số ưu điểm mà hệ thống có đượ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 3 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 2. Kiến thức nền tảng 2.1. Giới thiệu SMT Tính thỏa mãn là một trong những vấn đề quan trọng nhất của ngành khoa học máy tính. Các vấn đề cần tính thỏa mãn được ứng dụng trong cả phát triển phần cứng cũng như phần mềm, đặc biệt là kiểm định phần cứng, kiểm thử, lập lịch, đồ thị [3]. Trong các lĩnh vực nói trên, nhiều các ứng dụng được xây dựng dựa trên việc tạo ra các công thức tiền tố và việc chứng minh tính hợp lệ của chúng. Cho dù hai thập niên gần đây, việc chứng minh tính hợp lệ của các định lý, biểu thức tiền tố có những tiến bộ đáng kể, tuy nhiên, không phải công thức nào cũng có thể chứng minh một cách tự động được. Lý do của vấn đề này là bởi lẽ nhiều công thức không quan tâm đến tính khả thi trong trường hợp tổng quát mà chỉ được quan tâm trong một lý thuyết nền tảng [2,1]. Việc nghiên cứu tính khả thi của các công thức trong một lý thuyết nền tảng được gọi là các lý thuyết module về tính thỏa được (Satisfiability Modulo Theories hay SMT) và các công cụ để chứng minh một cách tự động các tính khả thi của những vẫn đề SMT được gọi là bộ giải SMT (SMT solver). Lý thuyết về SMT sẽ được đề cập cụ thể hơn trong phần giới thiệu về thư viện SMT. 2.2. Bộ giải SMT (SMT solver) Trên thực tế, việc xây dựng và sử dụng các bộ giải SMT được phát triển khá sớm, từ đầu những năm 1980. Tại thời điểm đó, một số bộ giải được xây dựng bởi Greg Nelson và Derek Oppent tại trường đại học Stanford , Robert Shostak tại SRI, và Robert Boyer và J Moore tại trường đại học ở Texas. Đến cuối những năm 1990, việc nghiên cứu SMT hiện đại dựa trên lợi thế của công nghệ SAT đã xây dựng nhiều bộ giải SMT tiến bộ hơn [4]. Như đã đề cập ở trên, trong khuôn khổ đồ án, việc đánh giá về tính đúng đắn, các nghiên cứu về thuật giải của từng bộ giải sẽ không được đề cập đến. Vấn đề đượ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 4 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 ra ở đây là kết quả của bộ giải nào sẽ được đưa ra sớm nhất. Hiện nay, có rất nhiều các bộ giải như Absolver, Boolector, CVC3, OpenSMT, Yices, Z3… Do yêu cầu của hệ thống là phải đưa ra được giá trị thỏa mãn (nếu bài toán SMT đó có thỏa mãn) nên bộ giải hệ thống sử dụng phải hỗ trợ chức năng này. Ngoài ra hệ thống sử dụng đầu vào theo chuẩn của SMT-Lib và ngắt thời gian giải một bài toán (trong trường hợp bài toán cần thời gian giải quá lớn), do đó, bộ giải cần phải có hỗ trợ những chức năng này khi hoạt động. Từ những yêu cầu đó, nhóm nghiên cứu và phát triển hệ thống đã quyết định sử dụng song song hai bộ giải là Yices của SRI International và Z3 của Microsoft. Hai bộ giải này tuy có cấu trúc khác nhau nhưng cùng được dựa trên thuật giải DPLL (Davis-Putnam-Logemann-Loveland) [5]. Việc tìm hiểu, phân tích cấu trúc cũng như thuật toán của hai bộ giải này sẽ không được đề cập cụ thể ở đây. 2.3. Thư viện SMT (SMT-LIB) Đề giải quyết các vấn đề SMT, việc nghiên cứu và đưa ra một chuẩn đầu vào là rất cần thiết. Thông thường, mỗi bộ giải SMT đều có một quy định riêng cho chuẩn đầu vào của mình, tuy nhiên như vậy sẽ thực sự khó khăn đối với việc thực thi một đầu vào bởi các bộ giải khác nhau. Vì vậy, việc nghiên cứu và đưa ra một chuẩn đầu vào thống nhất là rất cần thiết. Khoảng tháng tư năm 2004, Silvio Rainise và Cesare Tinelli đã đưa ra chuẩn về SMT-LIB đầu tiên [6]. Thời gian sau đó, họ liên tục cải tiến chuẩn đầu vào, bổ sung những quy định chuẩn, thuyết mới. Cho đến nay, hai tác giả này đã và đang xây dựng chuẩn SMT-LIB đã có phiên bản 2.0, tuy nhiên việc xây dựng đầu vào dựa trên chuẩn mới này chưa được phổ biến. Hầu hết các bộ giải cũng như đầu vào cho các vấn đề SMT-LIB đều được sử dụng bởi chuẩn 1.2 mà họ đã xây dựng vào khoảng tháng 8 năm 2006. 2.3.1. Cấu trúc cơ bản của SMT-LIB Như đã nói ở trên, vấn đề SMT là việc kiểm tra biểu thức logic φ có thỏa mãn được hay không trong lý thuyết nền T hay có một khuôn mẫu của T là khả thi. Vì vậy, kiến trúc cơ bản của một SMT-LIB thường bao gồm các vấn đề sau [7]: 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 5 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 - Một thủ tục logic cơ sở (underlying logic): Định dạng SMT-LIB hiện tại có hai định nghĩa về ngữ nghĩa của logic cơ sở. Thứ nhất là dịch nghĩa sang những biểu thức tiền tố cổ điển, có nghĩa là thủ tục của logic cơ sở giúp cho việc chuyển đổi sang khung làm việc của công cụ có sẵn hoặc giúp kiểm tra kết quả một cách dễ dàng hơn. Nghĩa thứ hai là chi phối ngữ nghĩa đại số dựa trên nhiều khuôn mẫu rút gọn. - Một lý thuyết nền (background theory): là những lý thuyết nền dùng để kiểm chứng tính thỏa mãn. Những lý thuyết cơ bản bao gồm lý thuyết số thực, lý thuyết mảng.. Phiên bản hiện tại của SMT-LIB chỉ hỗ trỡ những lý thuyết cơ bản này. - Một ngôn ngữ đầu vào (input language): Là lớp các biểu thức được chấp nhận như là đầu vào của SMT-LIB. 2.3.2. Khuôn dạng của SMT-LIB Một thư viện SMT được xây dựng theo chuẩn và dựa trên những định nghĩa sau (theo [7]): Định nghĩa 1 (Ký hiệu của SMT-LIB – SMT-LIB signature): Một ký hiệu SMT- LIB Σ là một bộ dữ liệu bao gồm: - Một tập không rỗng ∑ ⊆
 các ký hiệu phân cấp (sort symbol), một tập hợp ký hiệu hàm (function symbol) ∑ ⊆  và tập hợp các ký hiệu vị từ (predicate symbol) ∑ ⊆ ; - Một toàn ánh (total mapping) từ các biến (term variables) X tới ΣS; - Một quan hệ toàn phương (total relation) từ ΣF đến (ΣS)+, một chuỗi các thành phần của ΣS, không bao giờ có một cặp định dạng (f,s1…sns) và (f,s1…sns’) với s và s’ khác nhau; - Một quan hệ toàn phương từ ΣP tới (ΣS)*, thứ tự các thành phần ΣP. Định nghĩa 2 (Công thức trong SMT-LIB – SMT-LIB formula): Các công thức trong ngôn ngữ SMT-LIB là một tập hợp tất cả các công thức đúng cú pháp đóng (closed well-formed formula). 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 6 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 Định nghĩa 3 (khai báo lý thuyết – theory decl): chỉ tồn tại một khai báo lý thuyết trong một bài toán SMT-LIB và phải thỏa mãn những giới hạn sau: - Chúng bao gồm các khai báo của thuộc tính “sort” và “definition”; - Chúng chứa ít nhất một khai báo với một thuộc tính; - Không tồn tại khai báo định dạng f,s1…sns và f,s1…sns’ cho cùng một ký tự hàm f mà s và s’ khác nhau; - Tất cả các rút gọn trong khai báo ký tự hàm, vị từ được liệt kê trong khai báo thuộc tính “sort”; - Định nghĩa của lý thuyết được quy định trong thuộc tính “definition” và chỉ liên quan đến các khai báo ký tự phân cấp, ký tự hàm và ký tự vị từ; - Công thức trong thuộc tính “axiom” được xây dựng trên các khái báo ký tự trong các thuộc tính “sort”, “funs”, “pred”. Định nghĩa 4 (Khai báo Logic): Chỉ có một luật Logic được khai báo trong một bài toán SMT và phải được thỏa mãn các giới hạn sau: - Chúng bao gồm các khai báo thuộc tính “theory” và “language”; - Chúng chứa ít nhất một khai báo đối với một thuộc tính; - Giá trị của thuộc tính “theory” phải trùng với tên của thuyết T cho vài khai báo của DT trong SMT-LIB. Định nghĩa 5 (Khai báo về chuẩn): luật khai báo chuẩn phải thỏa mãn những giới hạn sau: - Chúng chứa chính xác một khai báo của thuộc tính “logic”, “formula” và “status”; - Giá trị của thuộc tính “logic” phải trùng khớp với tên của logic L cho vài khai báo DL trong SMT-LIB; - Mỗi một ký hiệu được khai báo trong thuộc tính “extrasorts”, “extrafuns” và “extrapred” cần phải là một phần của các ký hiệu được định nghĩa trong thuộc tính “language” của logic L; - Có thể có hơn một khai báo của thuộc tính “extrasort”; 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 7 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ó thể có hơn một khai báo của thuộc tính “extrafuns”, và mỗi thuộc tính “funs” của khai báo thuyết liên kết tới DL phải thỏa mãn yêu cầu 3 của định nghĩa 3; - Ký hiệu rút gọn trong khai báo “extrafuns” hoặc “extrapred” hoặc được khai báo trong “extrasort” hoặc thuộc về ký hiệu của logic L; - Công thức trong khai báo thuộc tính “assumption” và “formula” là ngôn ngữ của L và các ký hiệu của chúng được khai báo trong thuộc tính “extrasorts” “extrafuns” và “extrapred”. Từ những định nghĩa trên, việc xây dựng một bài toán SMT dựa trên chuẩn SMT-LIB sẽ theo cấu trúc sau [7]: Bảng 1: Luật sinh một toán hạng (1) ::= Chuỗi các ký tự, số, dấu chấm(.), nháy đơn(‘) và gạch dưới , bắt đầu bởi ký tự (2) ::= Bất kỳ chuỗ ký tự có thể in ra được (3) ::= {} (4) ::= 0 | chuỗi không rỗng các chữ số bắt đầu khác 0 (5) ::= .0* (6) ::= [(:)*] (7) ::= | (8) ::= ? (9) ::= $ (10) ::= : (11) ::= Chuỗi không rỗng các ký tự: =, >, <, &, @, #, +, -, *, /, %, |, ~ (12) ::= | (13) ::= | | distinct (14) ::= (15) ::= | (16) ::= | | | (17) ::= | ( +) | ( + *) | (ite *) 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 8 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 2: Luật sinh một công thức (1) ::= true | false | | (2) ::= | ( +) | ( + *) (3) ::= not | implies | if_then_else | and | or | xor | iff (4) ::= exists | forall (5) ::= ( ) (6) ::= | ( + * ) | ( + * ) | (let ( ) * ) | ( flet ( ) * ) Bảng 3: Luật sinh một thuyết (1) ::= chuỗi liên tiếp các ký tự (2) ::= “” (3) ::= ( + *) | ( *) | ( *) (4) ::= ( * *) (5) ::= (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.