Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | * | | GPUVerify: merge ElementEncodingRaceInstrumenter into RaceInstrumenter | 2012-06-22 | ||
| |/ / | ||||
| * | | GPUVerify: implement generic stride constraint generation | 2012-06-22 | ||
| | | | ||||
| * | | GPUVerify: make VarDefAnalysis capable of analysing non-constants | 2012-06-22 | ||
| | | | ||||
| * | | GPUVerify: construct BV*_AND and BV*_SUB using MakeBVFunctionCall | 2012-06-21 | ||
| | | | ||||
| * | | GPUVerify: replace MayBe{ThreadConfigurationVariable,Gid}Analyser with ↵ | 2012-06-21 | ||
| | | | | | | | | | | | | | | | | | | | | | simple functions based on VariableDefinitionAnalysis This also unbreaks the stride race instrumentation for various subtle reasons. | |||
* | | | Merge | 2012-06-21 | ||
|\ \ \ | ||||
| | * | | GPUVerify: make BuildNamedDefVisitor and SubstDualisedDefVisitor Duplicators | 2012-06-20 | ||
| |/ / | ||||
| * / | GPUVerify: fix constant offset invariant generation for the case where no ↵ | 2012-06-20 | ||
| |/ | | | | | | | constants are found | |||
| * | Move block predicator to VCGeneration | 2012-06-18 | ||
| | | ||||
| * | GPUVerify: block predicator: add a mode which disables procedure predicates | 2012-06-18 | ||
| | | | | | | | | | | This mode also conditionalises if statements to avoid problems with recursion. | |||
* | | Merge with dafny_runtime_checking | 2012-06-18 | ||
|\| | ||||
* | | Added command line option. | 2012-06-18 | ||
| | | ||||
| * | GPUVerify: implement is-a-constant analysis | 2012-06-15 | ||
| | | | | | | | | | | | | | | | | | | | | | | | | | | This analysis is used to generate race checking invariants for arbitrary (thread-level) constant offsets, in place of invariant generators for four specific constants (thread-id, global-id, 2D thread-id and 2D global-id) which are subsumed by the new analysis. The main motivation is to be able to recognise offsets used by word level accesses into byte arrays, which are formed from linear combinations of thread IDs and constants. This change allows us to remove the 2D and global size analyses, resulting in a 536-line net reduction in total code size. | |||
| * | GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant ↵ | 2012-06-15 | ||
| | | | | | | | | | | | | (e.g. consider a loop within a conditional) Pointed out by Ally. | |||
| * | GPUVerify: when dualising assume and assert statements, emit two statements ↵ | 2012-06-15 | ||
|/ | | | | instead of a conjunction | |||
* | Inter-thread race checking implementation done. | 2012-06-14 | ||
| | ||||
* | Fix for structured regions. | 2012-06-14 | ||
| | ||||
* | Progress on inter-group race checking | 2012-06-14 | ||
| | ||||
* | Merge | 2012-06-14 | ||
|\ | ||||
* | | Started work on inter-group race checking. | 2012-06-14 | ||
| | | ||||
| * | GPUVerify: the non-uniform loop invariant is not a candidate invariant | 2012-06-12 | ||
| | | | | | | | | Thanks to Ally for pointing this out. | |||
| * | GPUVerify: emit non-uniform loop candidate invariant | 2012-06-11 | ||
| | | ||||
| * | GPUVerify: emit "uniform loop" candidate invariant | 2012-06-11 | ||
| | | ||||
| * | GPUVerify: dualiser: preserve attributes of assert cmd | 2012-06-11 | ||
| | | | | | | | | This allows us to retain invariant tags. | |||
| * | GPUVerify: factor out CreateCandidateInvariant from AddCandidateInvariant | 2012-06-11 | ||
| | | | | | | | | | | This allows us to build candidate invariants in situations where we don't have a Region, such as the block predicator. | |||
| * | GPUVerify: initialise invariantGenerationCounter in the constructor, rather ↵ | 2012-06-11 | ||
|/ | | | | | | | than in ComputeInvariant This allows us to emit invariants in places earlier than ComputeInvariant (such as the block predicator). | |||
* | GPUVerify: teach the array control flow analyser to handle unstructured programs | 2012-06-08 | ||
| | ||||
* | GPUVerify: if one input file is supplied, choose output file name more ↵ | 2012-06-08 | ||
| | | | | | | | intelligently Specifically, if the input file's extension is not ".bpl", use its name (without extension) plus ".bpl" as the output file name. | |||
* | GPUVerify: fix line endings | 2012-06-08 | ||
| | ||||
* | GPUVerify: have StripThreadIdentifiers deal properly with identifiers ↵ | 2012-06-07 | ||
| | | | | containing a '$' | |||
* | GPUVerify: block predicator: use the name '_P' for the procedure predicate ↵ | 2012-06-07 | ||
| | | | | for consistency with the structured predicator | |||
* | GPUVerify: re-introduce the non-divergence check in unstructured mode | 2012-06-07 | ||
| | | | | This is OK now that we have assume stealing. | |||
* | GPUVerify: emit assumes for backedges | 2012-06-07 | ||
| | | | | | | Specifically, have the predicator emit backedge assumes with a :backedge attribute, and have the dualiser recognise such assumes and create an OR expression instead of an AND expression. | |||
* | GPUVerify: refactor candidate invariant generators and analyses to use regions | 2012-06-07 | ||
| | | | | | | | | | | | | | | | | The main goal of this change is to make the candidate invariant generation code and various analyses capable of handling both structured and unstructured programs. This is achieved using a high level abstraction of "regions" -- a region may either be a "root region" representing the entire implementation, or a natural loop within that implementation. Note that this is a subset to the term's meaning in the context of compilers, in which regions are also used for conditional control flow. Each region consists of a set of commands and a set of child regions. This change also has the side effect of eliminating a large amount of boilerplate code -- its net effect is to reduce the number of lines of code by 88. | |||
* | GPUVerify: recognise offsets in forms other than that produced by the old ↵ | 2012-06-01 | ||
| | | | | frontend | |||
* | GPUVerify: have dualiser reuse blocks | 2012-06-07 | ||
| | ||||
* | GPUVerify: add newly created barrier procedures to resolution context | 2012-06-07 | ||
| | ||||
* | GPUVerify: fix bug which caused us to log accesses at the end of the block, ↵ | 2012-06-06 | ||
| | | | | rather than the appropriate place | |||
* | GPUVerify: use Concat instead of PureCollections.Sequence.operator+ | 2012-05-31 | ||
| | ||||
* | GPUVerify: resolve barrier implementation in unstructured mode | 2012-05-31 | ||
| | | | | | Resolution of goto labels is required for the graph builder to work. | |||
* | GPUVerify: use a Formal for procedure predicates | 2012-05-31 | ||
| | ||||
* | GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ↵ | 2012-05-31 | ||
| | | | | multiple LHSs | |||
* | GPUVerify: implement assume stealing in block predicator | 2012-05-30 | ||
| | ||||
* | GPUVerify: disable barrier divergence check in unstructured mode for now | 2012-05-30 | ||
| | ||||
* | GPUVerify: have shared state abstraction, race instrumenter reuse blocks | 2012-05-30 | ||
| | | | | | Since we do not update transfer commands, they would otherwise refer to old blocks. | |||
* | GPUVerify: factor shared state abstraction for unstructured blocks | 2012-05-29 | ||
| | ||||
* | GPUVerify: factor the race instrumenter to handle unstructured blocks | 2012-05-29 | ||
| | ||||
* | GPUVerify: mark new work-item constants as non-unique | 2012-05-29 | ||
| | ||||
* | GPUVerify: in unstructured mode, disable uniformity analysis and return ↵ | 2012-05-25 | ||
| | | | | conservative results | |||
* | GPUVerify: implement a set of BV operation constructors which insert a ↵ | 2012-05-25 | ||
| | | | | function declaration if missing |