IR

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"] $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:

• fun[lib="pointer"] $set_default(obj: Pointer)
  • sets the leaf nodes of a variable to be the default value of zero
• fun[lib="pointer"] $apply(obj1: Pointer, op: Operation, obj2: Pointer, result: Pointer)
  • applies a binary operator op to two objects
• fun[lib="pointer"] $equals(x: Pointer, y: Pointer): Bool
• fun[lib="pointer"] $assert_equals(x: Pointer, y: Pointer, ...)
  • asserts that two objects are equal to each other
  • takes additional arguments for error message if the assertion is violated
• equality checking
• this function returns true iff the objects pointed to by the pointers x and y have the same type and value.

• fun[lib="pointer"] $contains(ptr1: Pointer, ptr2: Pointer): Bool
  • membership testing
  • 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.
• fun[lib="pointer"] $translate_ptr(ptr: Pointer, obj: Pointer): Pointer
  • pointer translation
  • 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.
• fun[lib="pointer"] $copy(ptr: Pointer, value: pointer)
  • copies the value pointed to by value to the memory location specified by ptr.
• 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>]
• fun[lib="pointer"] $set_leaf_nodes(obj: Pointer, value: Integer)
  • sets leaf nodes with the given value
• fun[lib="pointer"] $is_identity_ref(obj: Pointer)
  • checks if the given pointer is pointing to a variable
• fun[lib="pointer"] $leaf_nodes_equal_to(obj: Pointer, value: Integer)
  • checks if the leaf nodes of the given object are equal to the given integer value
• fun[lib="pointer"] $has_leaf_node_equal_to(obj: Pointer, value: Integer)
  • checks if the given object has a leaf node whose value is equal to the given integer value
• fun[lib="pointer"] $is_derefable_pointer(ptr: Pointer)
  • checks if the given pointer could be safely dereferenced
• fun[lib="pointer"] $pointer_add(ptr: Pointer, offset: Integer, type_size: Integer)
  • pointer addition

bundle utility

• Types
  • Bundle: a union type of all system types and user-defined types of a given program
• fun[lib="bundle", pure] $bundle_size(b: Bundle): Integer
  • returns the size of the given bundle
• fun[lib="bundle"] $bundle_pack(ptr: Pointer, size: Integer): Bundle
  • packs data into a bundle
• fun[lib="bundle"] $bundle_unpack(bundle: Bundle, ptr: Pointer)
  • unpack a bundle
• fun[lib="bundle"] $bundle_unpack_apply(data: Bundle, buf: Pointer, size: Integer, op: Operation)
  • unpack a bundle and apply some operation to the data

concurrency utility concurrency

barrier operations

• fun[lib="concurrency"] $gbarrier_create(scope: Scope, size: Integer): GBarrier
  • global barrier creation
• fun[lib="concurreny"] $gbarrier_destroy(barrier: Gbarrier)
  • global barrier destroy
• fun[lib="concurrency"] $barrier_create(scope: Scope, gbarrier: Gbarrier, place: Integer): Barrier
  • local barrier creation
• fun[lib="concurrency"] $barrier_destroy(barrier: Barrier)
  • local barrier destroy
• fun $barrier_call(barrier: Barrier)
  • barrier call

collective records

• Types
  • Collect_record
  • GCollect_checker
  • Collect_checker
• fun[lib="concurrency"] $gcollect_checker_create(scope: Scope): Gcollect_checker
  • global collective checker creation
• fun[lib="concurrency"] $gcollect_checker_destroy(gchecker: Gcollect_checker)
  • global collective checker destroy
• fun[lib="concurrency"] $collect_checker_create(scope: Scope, gchecker: Gcollect_checker)
  • collective checker creation
• fun[lib="concurrency"] $collect_checker_destroy(checker: Collect_checker)
  • collective checker destroy
• fun[lib="concurrency"] $collect_check(checker: Collect_checker, place: Integer, nprocs: Integer, entries: Bundle)
  • collective records checking

communication comm

• Types
  • Message
  • Queue
  • GComm
  • Comm
• message operations
  • fun[lib="comm"] $message_pack(src: Integer, dst: Integer, tag: Integer, dt: Pointer, sz: Integer): Message
    • pack a message
  • fun[lib="comm"] $message_unpack(msg: Message, buf: Pointer, sz: Integer)
    • unpack a message
  • fun[lib="comm", pure] $message_source(msg: Message): Integer
    • source of a message
  • fun[lib="comm", pure] $message_tag(msg: Message): Integer
    • tag of a message
  • fun[lib="comm", pure] $message_dest(msg: Message): Integer
    • destination of a message
  • fun[lib="comm", pure] $message_size(msg: Message): Integer
    • size of a message
• global communicator operations
  • fun[lib="comm"] $gcomm_create(scope: Scope, size: Integer): GComm
    • creation
  • fun[lib="comm"] $gcomm_destroy(gcomm: GComm)
    • destroy
  • fun[lib="comm"] $gcomm_dup(old: Comm, new: Comm)
    • duplication
• local communicator operations
  • fun[lib="comm"] $comm_create(scope: Scope, gcomm: GComm, place: Integer): Comm
    • creation
  • fun[lib="comm"] $comm_destroy(comm: Comm)
    • destroy
  • fun[lib="comm", pure] $comm_size(comm: Comm): Integer
    • returns the size of a communicator
  • fun[lib="comm", pure] $comm_place(comm: Comm): Integer
    • returns the place of the local communicator in the corresponding global communicator
  • fun[lib="comm"] $comm_enqueue(comm: Comm, msg: Message)
    • enqueue
  • fun[lib="comm", pure] $comm_probe(comm: Comm, src: Integer, tag: Integer): Bool
    • probe
  • fun[lib="comm"] $comm_seek(comm: Comm, src: Integer, tag: Integer): Message
    • seek
  • fun[lib="comm"] $comm_dequeue(comm: Comm, src: Integer, tag: Integer): Message
    • dequeue

domain utility domain

• Types
  • Domain_strategy
  • Domain_decomposition
• fun[lib="domain"] $domain_partition(dom: Domain, s: Domain_strategy, n: Integer): Domain_decomposition
  • domain decomposition
• funl[lib="domain"] $is_rectangular_domain(dom: Domain): Bool
  • checks if domain is rectangular
• fun[lib="domain", pure] $dimension_of(dom: Domain): Integer
  • returns the dimension of a domain
• fun[lib="domain"] $domain_size(dom: Domain): Integer
  • returns the size of a domain (i.e., total number of tuples)

sequence operations seq

• fun[lib="seq"] $seq_init(seq: Pointer, count: Integer, value: Pointer)
  • sequence initialization
  • 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
• fun[lib="seq", pure] $seq_length(seq: Pointer): Integer
  • returns the length of a sequence
• fun[lib="seq"] $seq_insert(seq: Pointer, index: Integer, values: Pointer, count: Integer)
  • insertion
• fun[lib="seq"] $seq_remove(seq: Pointer, index: Integer, values: Pointer, count: Integer)
  • removal
• fun[lib="seq"] $seq_append(seq: Pointer, values: Pointer, count: Integer)
  • appending