Dấu chấm phẩy rò rỉ
Author
Venue
Kỷ yếu Hội nghị ACM về Ngôn ngữ Lập trình 2021
Abstract
Logic và ngữ nghĩa chương trình kể một câu chuyện thú vị về cấu trúc tuần tự: khi thực thi (S1; S2), chúng ta thực thi S1 trước rồi mới đến S2. Tuy nhiên, để cải thiện hiệu suất, bộ xử lý thực thi các lệnh không theo thứ tự, và trình biên dịch sắp xếp lại các chương trình một cách thậm chí còn triệt để hơn. Theo thiết kế, các hệ thống đơn luồng không thể quan sát được những sự sắp xếp lại này; tuy nhiên, các hệ thống đa luồng thì có thể, khiến câu chuyện trở nên kém thú vị hơn đáng kể. Một nỗ lực chính thức để hiểu sự hỗn loạn này được gọi là "mô hình bộ nhớ linh hoạt". Các mô hình trước đây hoặc không giải quyết trực tiếp việc ghép nối tuần tự, hoặc hạn chế quá mức các bộ xử lý và trình biên dịch, hoặc cho phép các hành vi vô nghĩa không thể quan sát được trong thực tế. Để hỗ trợ việc ghép nối tuần tự đồng thời hướng đến phần cứng hiện đại, chúng tôi mở rộng phương pháp dựa trên sự kiện tiêu chuẩn bằng các điều kiện tiên quyết và các gia đình biến đổi mệnh đề. Khi tính toán ý nghĩa của (S1;S2), bộ chuyển đổi vị ngữ được áp dụng cho điều kiện tiên quyết của một sự kiện e từ S2 được chọn dựa trên tập hợp các sự kiện trong S1 mà e phụ thuộc vào. Chúng tôi áp dụng phương pháp này cho hai mô hình bộ nhớ hiện có.
