| 526 | | The CIVL core libraries include: |
| 527 | | |
| 528 | | * `civlc`: the basic library of CIVL, usually included in a CIVL-C program, defining types and functions that are frequently used; |
| 529 | | * `scope`: providing utility functions related to dynamic scopes; |
| 530 | | * `pointer`: providing utility functions dealing with pointers; |
| 531 | | * `seq`: providing operations on sequences which is realized using arrays; |
| 532 | | * `concurrency`: providing concurrency utilities such as barrier and collective record; |
| 533 | | * `bundle`: defining bundle types and their operations; |
| 534 | | * `comm`: defining communicators and their operations. |
| 535 | | |
| 536 | | === `civlc` : basic functions === |
| 537 | | |
| 538 | | Types: |
| 539 | | * `$operation`: an enumeration type of operations |
| 540 | | * `$int_iter`: integer iterator type ? |
| 541 | | |
| 542 | | Functions: |
| 543 | | * `fun[lib="civlc"] $set_default(obj: Pointer)` |
| 544 | | * sets the leaf nodes of a variable to be the default value of zero |
| 545 | | * `fun[lib="civlc"] $apply(obj1: Pointer, op: Operation, obj2: Pointer, result: Pointer)` |
| 546 | | * applies a binary operator `op` to two objects |
| 547 | | |
| 548 | | * elaborate an integer expression |
| 549 | | |
| 550 | | `fun[lib="civlc"] $elaborate(x: Integer)` |
| 551 | | |
| 552 | | * get a unique non-negative integer for time count |
| 553 | | |
| 554 | | `fun[lib="civlc"] $next_time_count()` |
| 555 | | |
| 556 | | * print path condition of the current state |
| 557 | | |
| 558 | | `fun[lib="civlc", pure] $pathCondition()` |
| 559 | | |
| 560 | | * non-deterministic choice of integer |
| 561 | | |
| 562 | | `fun[lib="civlc"] $choose_int(n: Integer): Integer;` |
| 563 | | |
| 564 | | This function takes as input a positive integer `n` and nondeterministicaly returns an integer in the range `[0, n − 1]`. |
| 565 | | |
| 566 | | * integer iterator operations |
| 567 | | * creation: `fun[lib="civlc"] $int_iter_create(scope: Scope, data: Pointer[Integer], size: int): Integer_iter` |
| 568 | | * has-next test: `fun[lib="civlc"] $int_iter_hasNext(iter: Integer_iter): Bool` |
| 569 | | * get next: `fun[lib="civlc"] $int_iter_next(iter: Integer_iter): Integer` |
| 570 | | * destroy: `fun[lib="civlc"] $int_iter_destroy(iter: Integer_iter)` |
| 571 | | |
| 572 | | * parent of a scope |
| 573 | | |
| 574 | | `fun[lib="scope"] $scope_parent(s: Scope): Scope` |
| 575 | | |
| 576 | | This function returns the parent dynamic scope of the dynamic scope referenced by `s`. If `s` is the root dynamic scope, it returns the `scope_null`. |
| 577 | | |
| 578 | | === Pointer utilities `pointer.cvh` === |
| 579 | | The header `pointer.cvh` declares functions taking pointers as the arguments for different purposes, including: |
| 580 | | |
| 581 | | * equality checking: |
| 582 | | `fun[lib="pointer"] $equals(x: Pointer, y: Pointer): Bool` |
| 583 | | this function returns true iff the objects pointed to by the pointers `x` and `y` have the same type and value. |
| 584 | | |
| 585 | | * membership testing: |
| 586 | | `fun[lib="pointer"] $contains(ptr1: Pointer, ptr2: Pointer): Bool` |
| 587 | | 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. |
| 588 | | |
| 589 | | * pointer translation: |
| 590 | | |
| 591 | | `fun[lib="pointer"] $translate_ptr(ptr: Pointer, obj: Pointer): Pointer` |
| 592 | | |
| 593 | | 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. |
| 594 | | |
| 595 | | * copy through pointers: |
| 596 | | `fun[lib="pointer"] $copy(ptr: Pointer, value: pointer)` |
| 597 | | |
| 598 | | copies the value pointed to by `value` to the memory location specified by `ptr`. |
| 599 | | |
| 600 | | * get leaf node pointers: |
| 601 | | |
| 602 | | `fun[lib="pointer"] $leaf_node_ptrs(array: Pointer, obj: Pointer)` |
| 603 | | |
| 604 | | 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>]` |
| 605 | | |
| 606 | | * set leaf nodes: |
| 607 | | `fun[lib="pointer"] $set_leaf_nodes(obj: Pointer, value: Integer)` |
| 608 | | |
| 609 | | * check if the given pointer is pointing to a variable: |
| 610 | | |
| 611 | | `fun[lib="pointer"] $is_identity_ref(obj: Pointer)` |
| 612 | | |
| 613 | | * check if the leaf nodes of the given object are equal to the given integer value |
| 614 | | |
| 615 | | `fun[lib="pointer"] $leaf_nodes_equal_to(obj: Pointer, value: Integer)` |
| 616 | | |
| 617 | | * check if the given object has a leaf node whose value is equal to the given integer value |
| 618 | | |
| 619 | | `fun[lib="pointer"] $has_leaf_node_equal_to(obj: Pointer, value: Integer)` |
| 620 | | |
| 621 | | * check if the given pointer could be safely dereferenced |
| 622 | | |
| 623 | | `fun[lib="pointer"] $is_derefable_pointer(ptr: Pointer)` |
| 624 | | |
| 625 | | * pointer addition |
| 626 | | `fun[lib="pointer"] $pointer_add(ptr: Pointer, offset: Integer, type_size: Integer)` |
| 627 | | |
| 628 | | === `bundle` utility === |
| 629 | | |
| 630 | | * Type: `Bundle`, which is a union type of all system types and user-defined types of a given program |
| 631 | | |
| 632 | | * size of bundle |
| 633 | | |
| 634 | | `fun[lib="bundle", pure] $bundle_size(b: Bundle): Integer` |
| 635 | | |
| 636 | | * pack data into a bundle |
| 637 | | |
| 638 | | `fun[lib="bundle"] $bundle_pack(ptr: Pointer, size: Integer): Bundle` |
| 639 | | |
| 640 | | * unpack a bundle |
| 641 | | |
| 642 | | `fun[lib="bundle"] $bundle_unpack(bundle: Bundle, ptr: Pointer)` |
| 643 | | |
| 644 | | * unpack a bundle and apply some operation to the data |
| 645 | | |
| 646 | | `fun[lib="bundle"] $bundle_unpack_apply(data: Bundle, buf: Pointer, size: Integer, op: Operation)` |
| 647 | | |
| 648 | | === concurrency utility `concurrency` === |
| 649 | | |
| 650 | | ==== barrier operations ==== |
| 651 | | * global barrier creation |
| 652 | | |
| 653 | | `fun[lib="concurrency"] $gbarrier_create(scope: Scope, size: Integer): GBarrier` |
| 654 | | |
| 655 | | * global barrier destroy |
| 656 | | |
| 657 | | `fun[lib="concurreny"] $gbarrier_destroy(barrier: Gbarrier)` |
| 658 | | |
| 659 | | * local barrier creation |
| 660 | | |
| 661 | | `fun[lib="concurrency"] $barrier_create(scope: Scope, gbarrier: Gbarrier, place: Integer): Barrier` |
| 662 | | |
| 663 | | * local barrier destroy |
| 664 | | |
| 665 | | `fun[lib="concurrency"] $barrier_destroy(barrier: Barrier)` |
| 666 | | |
| 667 | | * barrier call |
| 668 | | |
| 669 | | `fun $barrier_call(barrier: Barrier)` |
| 670 | | |
| 671 | | ==== collective records ==== |
| 672 | | * Type: `Collect_record`, `GCollect_checker`, and `Collect_checker` |
| 673 | | |
| 674 | | * global collective checker creation |
| 675 | | |
| 676 | | `fun[lib="concurrency"] $gcollect_checker_create(scope: Scope): Gcollect_checker` |
| 677 | | |
| 678 | | * global collective checker destroy |
| 679 | | |
| 680 | | `fun[lib="concurrency"] $gcollect_checker_destroy(gchecker: Gcollect_checker)` |
| 681 | | |
| 682 | | * collective checker creation |
| 683 | | |
| 684 | | `fun[lib="concurrency"] $collect_checker_create(scope: Scope, gchecker: Gcollect_checker)` |
| 685 | | |
| 686 | | * collective checker destroy |
| 687 | | |
| 688 | | `fun[lib="concurrency"] $collect_checker_destroy(checker: Collect_checker)` |
| 689 | | |
| 690 | | * collective records checking |
| 691 | | |
| 692 | | `fun[lib="concurrency"] $collect_check(checker: Collect_checker, place: Integer, nprocs: Integer, entries: Bundle)` |
| 693 | | |
| 694 | | === communication `comm` === |
| 695 | | * Types |
| 696 | | * `Message` |
| 697 | | * `Queue` |
| 698 | | * `GComm` |
| 699 | | * `Comm` |
| 700 | | |
| 701 | | * message operations |
| 702 | | * pack a message: `fun[lib="comm"] $message_pack(src: Integer, dst: Integer, tag: Integer, dt: Pointer, sz: Integer): Message` |
| 703 | | * unpack a message: `fun[lib="comm"] $message_unpack(msg: Message, buf: Pointer, sz: Integer)` |
| 704 | | * source of a message: `fun[lib="comm", pure] $message_source(msg: Message): Integer` |
| 705 | | * tag of a message: `fun[lib="comm", pure] $message_tag(msg: Message): Integer` |
| 706 | | * destination of a message: `fun[lib="comm", pure] $message_dest(msg: Message): Integer` |
| 707 | | * size of a message: `fun[lib="comm", pure] $message_size(msg: Message): Integer` |
| 708 | | |
| 709 | | * global communicator operations |
| 710 | | * creation: `fun[lib="comm"] $gcomm_create(scope: Scope, size: Integer): GComm` |
| 711 | | * destroy: `fun[lib="comm"] $gcomm_destroy(gcomm: GComm)` |
| 712 | | * duplication: `fun[lib="comm"] $gcomm_dup(old: Comm, new: Comm)` |
| 713 | | |
| 714 | | * local communicator operations |
| 715 | | * creation: `fun[lib="comm"] $comm_create(scope: Scope, gcomm: GComm, place: Integer): Comm` |
| 716 | | * destroy: `fun[lib="comm"] $comm_destroy(comm: Comm)` |
| 717 | | * get size: `fun[lib="comm", pure] $comm_size(comm: Comm): Integer` |
| 718 | | * get place: `fun[lib="comm", pure] $comm_place(comm: Comm): Integer` |
| 719 | | * enqueue: `fun[lib="comm"] $comm_enqueue(comm: Comm, msg: Message)` |
| 720 | | * probe: `fun[lib="comm", pure] $comm_probe(comm: Comm, src: Integer, tag: Integer): Bool` |
| 721 | | * seek: `fun[lib="comm"] $comm_seek(comm: Comm, src: Integer, tag: Integer): Message` |
| 722 | | * dequeue: `fun[lib="comm"] $comm_dequeue(comm: Comm, src: Integer, tag: Integer): Message` |
| 723 | | |
| 724 | | === domain utility `domain` === |
| 725 | | |
| 726 | | * Types: `Domain_strategy` and `Domain_decomposition` |
| 727 | | |
| 728 | | * domain decomposition: `fun[lib="domain"] $domain_partition(dom: Domain, s: Domain_strategy, n: Integer): Domain_decomposition` |
| 729 | | * check if domain is rectangular: `funl[lib="domain"] $is_rectangular_domain(dom: Domain): Bool` |
| 730 | | * get dimension: `fun[lib="domain", pure] $dimension_of(dom: Domain): Integer` |
| 731 | | * get size (total number of tuples): `fun[lib="domain"] $domain_size(dom: Domain): Integer` |
| 732 | | |
| 733 | | === sequence operations `seq` === |
| 734 | | * sequence initialization |
| 735 | | |
| 736 | | `fun[lib="seq"] $seq_init(seq: Pointer, count: Integer, value: Pointer)` |
| 737 | | |
| 738 | | 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: |
| 739 | | 1. array: pointer-to-incomplete-array-of-T |
| 740 | | 1. count: any integer type, must be nonnegative |
| 741 | | 1.value: pointer-to-T |
| 742 | | |
| 743 | | * length of sequence |
| 744 | | |
| 745 | | `fun[lib="seq", pure] $seq_length(seq: Pointer): Integer` |
| 746 | | |
| 747 | | * insertion |
| 748 | | |
| 749 | | `fun[lib="seq"] $seq_insert(seq: Pointer, index: Integer, values: Pointer, count: Integer)` |
| 750 | | |
| 751 | | * removal |
| 752 | | |
| 753 | | `fun[lib="seq"] $seq_remove(seq: Pointer, index: Integer, values: Pointer, count: Integer)` |
| 754 | | |
| 755 | | * appending |
| 756 | | |
| 757 | | `fun[lib="seq"] $seq_append(seq: Pointer, values: Pointer, count: Integer)` |
| 758 | | |
| 759 | | |
| | 526 | [wiki:Library_IR] |
