The CIVL core libraries include:

• civlc: the basic library of CIVL, usually included in a CIVL-C program, defining types and functions that are frequently used;
• scope: providing utility functions related to dynamic scopes;
• pointer: providing utility functions dealing with pointers;
• seq: providing operations on sequences which is realized using arrays;
• concurrency: providing concurrency utilities such as barrier and collective record;
• bundle: defining bundle types and their operations;
• comm: defining communicators and their operations.

civlc : basic functions

Types:

• $operation: an enumeration type of operations

Functions:

• fun[lib="civlc"] $set_default(obj: Pointer)
  • sets the leaf nodes of a variable to be the default value of zero
• fun[lib="civlc"] $apply(obj1: Pointer, op: Operation, obj2: Pointer, result: Pointer)
  • applies a binary operator op to two objects
• fun[lib="civlc"] $elaborate(x: Integer)
  • elaborate an integer expression
• fun[lib="civlc"] $next_time_count()
  • gets a unique non-negative integer for time count
• fun[lib="civlc", pure] $pathCondition()
  • prints path condition of the current state
• fun[lib="civlc"] $choose_int(n: Integer): Integer;
  • non-deterministic choice of integer
  • this function takes as input a positive integer n and nondeterministicaly returns an integer in the range [0, n − 1].
• fun[lib="scope"] $scope_parent(s: Scope): Scope
  • gets the parent of a scope s
  • If s is the root dynamic scope, it returns scope_null.

Pointer utilities pointer.cvh

The header pointer.cvh declares functions taking pointers as the arguments for different purposes, including:

• equality checking: fun[lib="pointer"] $equals(x: Pointer, y: Pointer): Bool this function returns true iff the objects pointed to by the pointers x and y have the same type and value.

• membership testing: fun[lib="pointer"] $contains(ptr1: Pointer, ptr2: Pointer): Bool this function returns true iff the object pointed to by ptr1 contains the object pointed to by ptr2. For example, $contains(&a, &a[1].x) would return true.

• pointer translation:

fun[lib="pointer"] $translate_ptr(ptr: Pointer, obj: Pointer): Pointer

this function returns a pointer which is the result of translating the pointer ptr (a pointer into one object) to a pointer into a different object obj with similar structure.

• copy through pointers: fun[lib="pointer"] $copy(ptr: Pointer, value: pointer)

copies the value pointed to by value to the memory location specified by ptr.

• get leaf node pointers:

fun[lib="pointer"] $leaf_node_ptrs(array: Pointer, obj: Pointer)

copies the references to the leaf nodes of obj to the given array. The type of obj is Pointer[T'], all leaf nodes of T' has type T, and array has type Pointer[Array[T]]. For example, T' could be Tuple[<Integer, Array[Integer], Integer>]

• set leaf nodes: fun[lib="pointer"] $set_leaf_nodes(obj: Pointer, value: Integer)

• check if the given pointer is pointing to a variable:

fun[lib="pointer"] $is_identity_ref(obj: Pointer)

• check if the leaf nodes of the given object are equal to the given integer value

fun[lib="pointer"] $leaf_nodes_equal_to(obj: Pointer, value: Integer)

• check if the given object has a leaf node whose value is equal to the given integer value

fun[lib="pointer"] $has_leaf_node_equal_to(obj: Pointer, value: Integer)

• check if the given pointer could be safely dereferenced

fun[lib="pointer"] $is_derefable_pointer(ptr: Pointer)

• pointer addition fun[lib="pointer"] $pointer_add(ptr: Pointer, offset: Integer, type_size: Integer)

bundle utility

• Type: Bundle, which is a union type of all system types and user-defined types of a given program

• size of bundle

fun[lib="bundle", pure] $bundle_size(b: Bundle): Integer

• pack data into a bundle

fun[lib="bundle"] $bundle_pack(ptr: Pointer, size: Integer): Bundle

• unpack a bundle

fun[lib="bundle"] $bundle_unpack(bundle: Bundle, ptr: Pointer)

• unpack a bundle and apply some operation to the data

fun[lib="bundle"] $bundle_unpack_apply(data: Bundle, buf: Pointer, size: Integer, op: Operation)

concurrency utility concurrency

barrier operations

• global barrier creation

fun[lib="concurrency"] $gbarrier_create(scope: Scope, size: Integer): GBarrier

• global barrier destroy

fun[lib="concurreny"] $gbarrier_destroy(barrier: Gbarrier)

• local barrier creation

fun[lib="concurrency"] $barrier_create(scope: Scope, gbarrier: Gbarrier, place: Integer): Barrier

• local barrier destroy

fun[lib="concurrency"] $barrier_destroy(barrier: Barrier)

• barrier call

fun $barrier_call(barrier: Barrier)

collective records

• Type: Collect_record, GCollect_checker, and Collect_checker

• global collective checker creation

fun[lib="concurrency"] $gcollect_checker_create(scope: Scope): Gcollect_checker

• global collective checker destroy

fun[lib="concurrency"] $gcollect_checker_destroy(gchecker: Gcollect_checker)

• collective checker creation

fun[lib="concurrency"] $collect_checker_create(scope: Scope, gchecker: Gcollect_checker)

• collective checker destroy

fun[lib="concurrency"] $collect_checker_destroy(checker: Collect_checker)

• collective records checking

fun[lib="concurrency"] $collect_check(checker: Collect_checker, place: Integer, nprocs: Integer, entries: Bundle)

communication comm

• Types
  • Message
  • Queue
  • GComm
  • Comm

• message operations
  • pack a message: fun[lib="comm"] $message_pack(src: Integer, dst: Integer, tag: Integer, dt: Pointer, sz: Integer): Message
  • unpack a message: fun[lib="comm"] $message_unpack(msg: Message, buf: Pointer, sz: Integer)
  • source of a message: fun[lib="comm", pure] $message_source(msg: Message): Integer
  • tag of a message: fun[lib="comm", pure] $message_tag(msg: Message): Integer
  • destination of a message: fun[lib="comm", pure] $message_dest(msg: Message): Integer
  • size of a message: fun[lib="comm", pure] $message_size(msg: Message): Integer

• global communicator operations
  • creation: fun[lib="comm"] $gcomm_create(scope: Scope, size: Integer): GComm
  • destroy: fun[lib="comm"] $gcomm_destroy(gcomm: GComm)
  • duplication: fun[lib="comm"] $gcomm_dup(old: Comm, new: Comm)

• local communicator operations
  • creation: fun[lib="comm"] $comm_create(scope: Scope, gcomm: GComm, place: Integer): Comm
  • destroy: fun[lib="comm"] $comm_destroy(comm: Comm)
  • get size: fun[lib="comm", pure] $comm_size(comm: Comm): Integer
  • get place: fun[lib="comm", pure] $comm_place(comm: Comm): Integer
  • enqueue: fun[lib="comm"] $comm_enqueue(comm: Comm, msg: Message)
  • probe: fun[lib="comm", pure] $comm_probe(comm: Comm, src: Integer, tag: Integer): Bool
  • seek: fun[lib="comm"] $comm_seek(comm: Comm, src: Integer, tag: Integer): Message
  • dequeue: fun[lib="comm"] $comm_dequeue(comm: Comm, src: Integer, tag: Integer): Message

domain utility domain

• Types: Domain_strategy and Domain_decomposition

• domain decomposition: fun[lib="domain"] $domain_partition(dom: Domain, s: Domain_strategy, n: Integer): Domain_decomposition
• check if domain is rectangular: funl[lib="domain"] $is_rectangular_domain(dom: Domain): Bool
• get dimension: fun[lib="domain", pure] $dimension_of(dom: Domain): Integer
• get size (total number of tuples): fun[lib="domain"] $domain_size(dom: Domain): Integer

sequence operations seq

• sequence initialization

fun[lib="seq"] $seq_init(seq: Pointer, count: Integer, value: Pointer)

given a pointer to an object of Array[T], sets that object to be the array of length count in which every element has the same value, specified by the given pointer value.Parameters:

1. array: pointer-to-incomplete-array-of-T
2. count: any integer type, must be nonnegative 1.value: pointer-to-T

• length of sequence

fun[lib="seq", pure] $seq_length(seq: Pointer): Integer

• insertion

fun[lib="seq"] $seq_insert(seq: Pointer, index: Integer, values: Pointer, count: Integer)

• removal

fun[lib="seq"] $seq_remove(seq: Pointer, index: Integer, values: Pointer, count: Integer)

• appending

fun[lib="seq"] $seq_append(seq: Pointer, values: Pointer, count: Integer)