Changes between Version 19 and Version 20 of Introduction


Ignore:
Timestamp:
12/31/18 14:56:11 (7 years ago)
Author:
siegel
Comment:

--

Legend:

Unmodified
Added
Removed
Modified

  • Introduction

    v19 v20  
    22= Contents =
    33
    4 * [#intro Introduction]
    5 * [#lang Language]
    6 * [#semantics Semantics]
    7 * [#tools Tools]
    8 
    9 = Introduction = #intro
    10 
    11 == What is CIVL? ==
     4[[PageOutline]]
     5
     6= What is CIVL? =
    127
    138CIVL stands for ''Concurrency Intermediate Verification Language''.  The CIVL platform encompasses:
    … …  
    4843
    4944
    50 == Verifying  Different Kinds of Programs ==
    51 
    52 === Verifying CIVL-C Programs ===
     45= Verifying CIVL-C Programs =
    5346
    5447Dijkstra’s well-known Dining Philosophers system can be encoded in CIVL-C as follows:
    … …  
    425418
    426419
    427 === Verifying Sequential C Programs ===
     420= Verifying Sequential C Programs =
    428421
    429422Since almost anything you can do in sequential C is also legal CIVL-C, there is not much you have to do to apply the verifier to C programs.
    … …  
    582575There are limitations to the application of CIVL to C programs.   Support for the standard library is only partial.   Small bounds will have to be placed on many parameters in order for CIVL verification to terminate (or terminate in a reasonable amount of time). 
    583576
    584 === Verifying C/MPI Programs ===
     577= Verifying C/MPI Programs =
    585578
    586579CIVL 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.
    … …  
    600593
    601594
    602 === Verifying C/OpenMP Programs ===
     595= Verifying C/OpenMP Programs =
    603596
    604597CIVL uses an input variable `omp_thread_max` for verifying OpenMP programs.   It must be specified on the command line, e.g.,
    … …  
    614607A serious limitation in the current OpenMP transformation is that access to shared variables cannot take place through pointers.
    615608
    616 === Verifying CUDA-C Programs ===
    617 
    618 
    619 
    620 === Verifying C/Pthreads Programs ===
    621 
    622 
    623 
    624 === Verifying Fortran Programs ===
     609= Verifying CUDA-C Programs =
     610
     611
     612
     613= Verifying C/Pthreads Programs =
     614
     615
     616
     617= Verifying Fortran Programs =
    625618
    626619
    … …  
    628621(under development)
    629622
    630 
    631 
    632 = The CIVL-C Language = #lang
    633 
    634 
    635 
    636 = Semantics = #semantics
    637 
    638 
    639 = Command-line Tools = #tools