Skip to main content

creusot_std/std/sync/
fence.rs

1use creusot_std::{
2    prelude::*,
3    std::sync::view::{AcquireSyncView, ReleaseSyncView, SyncView},
4};
5
6use std::sync::atomic::{Ordering, fence};
7
8#[ensures(*sync_view == result@)]
9#[trusted]
10#[allow(unused_variables)]
11pub fn fence_release(sync_view: Ghost<SyncView>) -> Ghost<ReleaseSyncView> {
12    fence(Ordering::Release);
13    Ghost::conjure()
14}
15
16#[ensures(acq_view@ == *result)]
17#[trusted]
18#[allow(unused_variables)]
19pub fn fence_acquire(acq_view: Ghost<AcquireSyncView>) -> Ghost<SyncView> {
20    fence(Ordering::Acquire);
21    Ghost::conjure()
22}