Lý luận đại số về tính kịp thời
Algebraic Reasoning About Timeliness.
Việc thiết kế các hệ thống phân tán để có hiệu suất có thể dự đoán được khi chịu tải cao là rất khó do cạn kiệt tài nguyên, phi tuyến tính và hành vi ngẫu nhiên. Tính kịp thời, nghĩa là cung cấp kết quả trong giới hạn thời gian xác định, là khía cạnh trung tâm của hiệu suất có thể dự đoán được. Trong tài liệu này, các tác giả tập trung vào tính kịp thời bằng cách sử dụng mô hình Phát triển hệ thống ∆Q (∆QSD, do PNSol phát triển), tính toán tính kịp thời bằng cách lập mô hình hệ thống dựa trên quan sát bằng cách sử dụng biểu thức kết quả. Biểu thức kết quả là một định nghĩa tổng hợp về hành vi được quan sát của hệ thống xét về các hoạt động cơ bản của nó. Với hành vi của các hoạt động cơ bản, ∆QSD tính toán một cách hiệu quả hành vi ngẫu nhiên của toàn bộ hệ thống bao gồm cả tính kịp thời. Tài liệu này chính thức chứng minh thuộc tính đại số hữu ích của các biểu thức kết quả với tính kịp thời. Các tác giả chứng minh các cấu trúc đại số khác nhau mà tập hợp các biểu thức kết quả hình thành bằng các toán tử ∆QSD khác nhau và chứng minh tại sao các toán tử đó không tạo thành các cấu trúc phong phú hơn. Các tác giả chứng minh hoặc bác bỏ tập hợp tất cả các kết quả phân phối có thể có trên biểu thức kết quả. Trong quá trình bác bỏ 8 kết quả phân phối trong số đó, các tác giả phát triển kỹ thuật chuẩn hóa, giúp phát triển phần đầu tiên của toán học về các biến ngẫu nhiên chưa chuẩn hóa. Cuối cùng, các tác giả cũng chứng minh 14 phương trình đã được sử dụng trước đây trong ∆QSD thực tiễn. Lợi ích trước mắt là viết lại các quy tắc có thể được sử dụng để thăm dò thiết kế theo phương trình về tính kịp thời đã được thiết lập. Công việc này là một phần của dự án đang diễn ra nhằm phổ biến và xây dựng công cụ hỗ trợ cho ∆QSD. Khả năng viết lại các biểu thức kết quả là cần thiết để hỗ trợ công cụ hiệu quả.
Đọc thêm các bài viết liên quan tại thẻ Tags bên dưới