apps/mutex/mutex.camkes

/*
 * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 */

import <std_connector.camkes>;

import "components/A/A.camkes";
import "components/B/B.camkes";

connector seL4MyConnector {
    from Procedure;
    to Procedure;

    attribute string isabelle_connector_spec = "\<lparr>
        connector_type = NativeConnector,
        connector_interface = RPCInterface,
        connector_access = \<lparr>
            access_from_to   = {},
            access_to_from   = {},
            access_from_from = {},
            access_to_to     = {},
            access_from_conn = {Reset, SyncSend, Receive},
            access_to_conn   = {Reset, SyncSend, Notify, Receive}
        \<rparr> \<rparr>";
}

assembly {
    composition {
        component A a;
        component B b;

        connection seL4MyConnector simple(from a.lock, to b.lock);
    }
}