Changes between Initial Version and Version 1 of Library_IR

Timestamp:

12/10/15 14:30:02 (10 years ago)

Author:

zmanchun

Comment:

--

Library_IR

@@ +1 @@
+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
+    1. 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)`