Struct ConcurrentSeparationLogic 

pub struct ConcurrentSeparationLogic {
    pub threads: Vec<String>,
}

Concurrent separation logic for parallel programs.

Fields

threads: Vec<String>

Implementations

impl ConcurrentSeparationLogic

pub fn new(threads: Vec<String>) -> Self

pub fn rely_guarantee(&self) -> String

Describe the Rely-Guarantee method for concurrent reasoning.

pub fn permission_accounting(&self) -> String

Describe permission accounting (fractional permissions).