Changes between Version 17 and Version 18 of Challenge

Timestamp:

03/12/19 11:30:30 (7 years ago)

Author:

siegel

Comment:

--

Challenge

@@ -191 +191 @@
 }
 }}}
+
+== An example MPI program ==
 
 {{{
@@ -222 +224 @@
 }}}
 
+
+== Verifying C/MPI Programs ==
+
+CIVL can verify C/MPI programs that use a subset of MPI.    The instructions for sequential programs apply equally to MPI programs.  In addition, one must specify either (1) the number of processes for the MPI program, or (2) an upper and a lower bound on the number of processes for the MPI program.
+
+In the following example, the C/MPI program `ring.c` is verified for exactly 5 processes:
+
+{{{
+civl verify -input_mpi_nprocs=5 ring.c
+}}}
+
+In the following example, `ring.c` is verified for any number of processes between 2 and 5, inclusive:
+
+{{{
+civl verify -input_mpi_nprocs_lo=2 -input_mpi_nprocs_hi=5 ring.c
+}}}
+
+