Benchmark for work "Temporal Verification of Mixed Sync-Async Execution Models"

This benchmark is for validation and evaluation purpose for the work "Temporal Verification of Mixed Sync-Async Execution Models". It is constructed by manually annotating ASyncEffs specifications, including both succeeded and failed cases. This benchmark consists two folders: 1. validation_tests: The validation tests are synthetic examples to test the main contributions, including the preemption interleaving computation and the inclusion checking for the parallel composition and the waiting operator. 2. evaluation_tests: We select 16 programs, varying from 15 lines to 300 lines, and annotate ASyncEffs specifications with a 1:1 ratio for succeeded/failed cases.