include/builtin/std_connector.camkes

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

import "camkes-hardware.idl4";
import "gdb-delegate.camkes";

/**
 * @file
 *
 * This file defines a list of connectors. A connection is an instance of a
 * connector, allowing two components to communicate with each other.
 * Different connectors are used for different purposes.
 *
 * In essence, a connector defines how exactly a component connects to another
 * component. There are two parts, from and to. Most of the connectors are
 * defined such that the "from" component sends data to the "to" component. So
 * the "from" component is more like a sender and the "to" component is like a
 * receiver. Having said that, a totally different semantic can be implemented.
 * It's really up to the programmer to decide it.
 *
 * To use the connector, you define it like this:
 *
 *    connection RPC util_fatfs_FS(from util.fs, to fatfs.fs);
 *
 * where the util_fatfs_FS connection is an instance of the RPC connector. It
 * connects util.fs interface to fatfs.fs interface.
 */

/**
 * Asynchronous event connector
 *
 * Once the connection has been established, the consumer could wait for
 * asynchronous signal sending from the emitter. The waiting process can be
 * blocked or non-blocked. The sending process is non-blocked, that is the
 * emitter can send data at any time and at any rate.
 *
 * One of the advantages of this connector is if the consumer executes much
 * faster than the emitter. The consumer could do other stuff while waiting for
 * the asynchronous signal from the emitter. However it's harder to synchronize
 * the components.
 */
connector seL4Notification {
    from Event with 0 threads;
    to Events;
    attribute string isabelle_connector_spec = "seL4Notification"; /* builtin connector */
}
connector seL4NotificationBind {
    from Events with 0 threads;
    to Event;
}
connector seL4NotificationQueue {
    from Event with 0 threads;
    to Events;
}
connector seL4NotificationNative {
    from Events with 0 threads;
    to Event;
}

/**
 * Asynchronous RPC event connector
 *
 * This connector works exactly the same as the asynchronous event connector.
 * The consumer and emitter shouldn't notice any difference. But the internal
 * implementation is different. seL4Notification uses the asynchronous
 * mechanism to send signal, whereas seL4RPCEvent uses the regular RPC
 * to send and imitate the event signal.
 */
connector seL4RPCEvent {
    from Event;
    to Event;
}

/**
 * RPC connector
 *
 * Once the connection has been established, the user could wait for regular
 * RPC signal sending from the provider. The sending and waiting phase are
 * blocked.
 */
connector seL4RPCCall {
    from Procedures with 0 threads;
    to Procedure;
    attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */
}
connector cantripRPCCall {
    from Procedures with 0 threads;
    to Procedure;
    attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */
}

/* Same as seL4RPCCall, except has relaxed type checking */
connector seL4RPCCallNoType {
    from Procedures with 0 threads;
    to Procedure;
    attribute bool disable_interface_type_checking = true;
    attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */
}

/**
 * Direct Call connector
 *
 * Situates both components in the same protection domain, so that interface
 * calls are backed by function calls, rather than RPCs.
 */
connector seL4DirectCall {
    from Procedure;
    to Procedure;
    attribute string isabelle_connector_spec = "seL4RPC"; /* builtin connector */
}

/**
 * Dataport connector
 *
 * This connector allows memory sharing between two components.
 *
 * The dataport size is not defined in this connector, it's up to the
 * implementation.
 */
connector seL4SharedData {
    from Dataports with 0 threads;
    to Dataports with 0 threads;
    attribute string isabelle_connector_spec = "seL4SharedData"; /* builtin connector */
}
connector cantripSharedData {
    from Dataports with 0 threads;
    to Dataports with 0 threads;
    attribute string isabelle_connector_spec = "seL4SharedData"; /* builtin connector */
}

/**
 * Hardware MMIO dataport connector
 *
 * This connector has special behaviour: it designates the component on the
 * hardware_component_data side as fictitious, and represents a hardware
 * device. Code will therefore not be generated for that component.
 *
 * It also implies that the backing memory will be mapped uncached.
 *
 * The hardware_component_data dataport's attribute string should consist of
 * the physical address and size of the memory window, in the following format:
 * "0x<address>:0x<size>"
 */
connector seL4HardwareMMIO {
    from Dataports with 0 threads;
    to hardware Dataport;
    attribute string isabelle_connector_spec = "seL4HardwareMMIO"; /* builtin connector */
}
connector cantripMMIO {
    from Dataports with 0 threads;
    to hardware Dataport;
    attribute string isabelle_connector_spec = "seL4HardwareMMIO"; /* builtin connector */
}

/**
 * Hardware interrupt event connector
 *
 * This connector has special behaviour: it designates the component on the
 * hardware_component_interrupt side as fictitious, and represents a hardware
 * device. Code will therefore not be generated for that component.
 *
 * The hardware_component_interrupt event's attribute string should consist of
 * the interrupt number, in either decimal or (with the "0x" prefix)
 * hexadecimal.
 */
connector seL4HardwareInterrupt {
    from hardware Event;
    to Event;
    attribute string isabelle_connector_spec = "seL4HardwareInterrupt"; /* builtin connector */
}
connector seL4IOAPICHardwareInterrupt {
    from hardware Event;
    to Event;
}
/**
 * CantripOS supports connecting multiple IRQ's to a single endpoint using
 * the usual syntax; e.g.
 *
 *  connection cantripIRQ foo(from srcA, from srcB, ..., to dest);
 *
 * Interrupt events are always badged with a bitmask of enumerated value;
 * e.g. for the above example, badge srcA = 1<<0, badge srcB = 1<<1, ...
 */
connector cantripIRQ {
    from hardware Events with 0 threads;
    to Event;
    attribute string isabelle_connector_spec = "seL4HardwareInterrupt"; /* builtin connector */
}

/**
 * Hardware IOPorts connector
 *
 * This connector has special behaviour: it designates the component on the
 * hardware_component_data side as fictitious, and represents a hardware
 * device. Code will therefore not be generated for that component.
 *
 * Note that by nature, this connector is ia32-specific.
 *
 * The attribute 'hardware_component_port_attributes' should be set to define the
 * the IOPort range needed, in the following format: "0x<first_port>:0x<last_port>".
 * The interface provided should be "IOPort". E.g.
 *  component foo {
 *      hardware;
 *      provides IOPort bar;
 *  }
 *  assembly {
 *      composition {
 *          component foo f;
 *          ...
 *          connection HardwareIOPort moo(from ..., to foo.bar);
 *      }
 *      configuration {
 *          foo.bar_attributes = "0x42:0x84";
 *      }
 *  }
 */
connector seL4HardwareIOPort {
    from Procedure with 0 threads;
    to hardware Procedure;
}

/**
 * DTB hardware connector
 *
 * This connector allows a user to automatically generate the resources needed to
 * interact with a device. This includes memory-mapped hardware registers and interrupts.
 * It does so by reading from a specified DTB node.

 * To use this connector, a dummy 'emits' interface needs to be created. For each 
 * pair of hardware registers and/or interrupts, you wish to initialise, a 'consumes'
 * interface needs to be created and paired with the dummy source. E.g.
 *  
 *  consumes Dummy timer;
 *  consumes Dummy serial;
 *  emits Dummy dummy_source;
 *      ...
 *  connection seL4DTBHardware timer_conn(from dummy_source, to timer);
 *  connection seL4DTBHardware timer_conn(from dummy_source, to serial);
 * 
 * To pass in a DTB node to the connector, the attribute 'dtb' of the 'consumes' 
 * interface must be set to the DTB path of a particular node. E.g.
 *
 *  timer.dtb = dtb({ "path" : "/soc/serial@deadbeef" });
 * 
 * Interrupts will not be generated by default. To generate interrupts, set the
 * 'generate_interrupts' attribute of the 'consumes' interface to equal to '1'. E.g.
 * 
 *  timer.generate_interrupts = 1;
 *
 * Warning: The connector currently assumes that the `interrupts` binding in the DTB
 * node follow the format of the ARM GIC, i.e. cell 1 = SPI interrupt, 
 * cell 2 = interrupt number and cell 3 = interrupt flag.
 *
 */
connector seL4DTBHardware {
    from Event with 0 threads;
    to Events;

    /* This connector by itself confers no access rights. Use other
     * attributes to specify integrity policy for hardware. */
    attribute string isabelle_connector_spec = "\<lparr>
        connector_type = NativeConnector,
        connector_interface = EventInterface,
        connector_access = \<lparr>
            access_from_to   = {},
            access_to_from   = {},
            access_from_from = {},
            access_to_to     = {},
            access_from_conn = {},
            access_to_conn   = {}
        \<rparr> \<rparr>";
}

connector seL4DTBHW {
    from hardware Event;
    to Events;
}

connector seL4InitHardware {
    from Event with 0 threads;
    to Events with 0 threads;
}

/**
 * Dataport connector
 *
 * This connector defines a shared DMA pool between multiple components.
 *
 * Supported config options:
 *
 * Connector instance level:
 * paddr: Specify a physical address for the Pool to start at. Default: Any
 * size: Specify the size of the pool.  Default: 4096
 * controller: Identify the interface instance that is allowed to make allocations.
 *
 * Interface instance level:
 * %{interface_name}_cached: Cache attributes of the pool's mapping. Default: True
 * %{interface_name}_access: Memory permissions of the pool's mapping. Default: RWXP (All)
 *
 */
connector seL4DMASharedData {
    from Dataports with 0 threads;
    to Dataports with 0 threads;
    attribute string isabelle_connector_spec = "seL4SharedData"; /* builtin connector */
}

/**
 * RPCCallSignal connector
 *
 * This connector is like the regular RPCCall connector, except that
 * there is a Notification endpoint allocated and associated with the 
 * connector. The Notification endpoint is a 1-to-n relationship in that
 * a component connected to many other components on the same interface
 * with this connector is able to signal the connected components individually.
 *
 * It requires an attribute to define a badge for it to use and to couple
 * the RPC connector and the associated dataport. The badge can be any
 * unique number.
 * 	<from_component>.<from_interface>_attributes = "<badge>";
 *
 * The 'from' side of the connector can access the associated Notification
 * endpoint via this exposed function:
 *      seL4_CPtr <interface name>_notification(void);
 *
 * The 'to' side of the connector can signal the desired connected component
 * by passing the component's badge into the following function:
 *      void <interface_name>_emit(unsigned int badge);
 * There is also a function to query the largest badge of all the connected
 * components:
 *      int <interface_name>_largest_badge(void);
 */
connector cantripRPCCallSignal {
    from Procedures;
    to Procedure;
    attribute bool from_global_endpoint = True;
}

/**
 * cantripRPCOverMultiSharedData connector
 *
 * This connector is similar to seL4RPCCall but will use shared memory instead of
 * the IPC buffer to transfer data between components. It supports multiple clients
 * communicating with a single server. Each client has a separate shared memory region
 * with the server. The size of the shared memory region can be configured on a
 * per-client basis via setting ${client_instance}.${interface_name}_shmem_size.
 * The default shared memory size is 4096 bytes.
 * For a multi-threaded caller, subsequent calls to the interface will block until
 * the first call returns in order to preserve the integrity of the shared buffer.
 *
 */
connector cantripRPCOverMultiSharedData {
    from Procedures with 0 threads;
    to Procedure;
}

/**
 * cantripRPCSignalOverMultiSharedData connector
 *
 * Combination of cantripRPCOverMultiSharedData & cantripRPCCallSignal.
 */
connector cantripRPCSignalOverMultiSharedData {
    from Procedures with 0 threads;
    to Procedure;
    attribute bool from_global_endpoint = True;
}