← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to PetriEngine/Structures/linked_bucket.h

  • Committer: srba.jiri at gmail
  • Date: 2020-09-11 14:23:39 UTC
  • mfrom: (213.1.151 interval_tar)
  • Revision ID: srba.jiri@gmail.com-20200911142339-bq9328s1gppw24uj
merged in lp:~verifypn-maintainers/verifypn/interval_tar doing 
- Implements TAR w/o z3, but using a simple integer inference engine for Hoare logic.
 - Replaces LP-Solve with GLPK, reduces computation-time and memory overhead
 - Implements new global properties, translated into CTL formulae.

Show diffs side-by-side

added added

removed removed

Lines of Context:
PetriEngine/Structures/linked_bucket.h
1
 
/* VerifyPN - TAPAAL Petri Net Engine
2
 
 * Copyright (C) 2016  Peter Gjøl Jensen <root@petergjoel.dk>
3
 
 * 
4
 
 * This program is free software: you can redistribute it and/or modify
5
 
 * it under the terms of the GNU General Public License as published by
6
 
 * the Free Software Foundation, either version 3 of the License, or
7
 
 * (at your option) any later version.
8
 
 * 
9
 
 * This program is distributed in the hope that it will be useful,
10
 
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
11
 
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
12
 
 * GNU General Public License for more details.
13
 
 * 
14
 
 * You should have received a copy of the GNU General Public License
15
 
 * along with this program.  If not, see <http://www.gnu.org/licenses/>.
16
 
 */
17
 
 
18
 
/* 
19
 
 * File:   linked_bucket.h
20
 
 * Author: Peter G. Jensen
21
 
 *
22
 
 * Created on 07 June 2016, 21:51
23
 
 */
24
 
#include <stdlib.h>
25
 
#include <assert.h>
26
 
#include <atomic>
27
 
#include <vector>
28
 
#include <iostream>
29
 
 
30
 
#ifndef LINKED_BUCKET_H
31
 
#define LINKED_BUCKET_H
32
 
 
33
 
template<typename T, size_t C>
34
 
class linked_bucket_t {
35
 
private:
36
 
 
37
 
    struct bucket_t {
38
 
        std::atomic<bucket_t*> _nbucket;
39
 
        std::atomic<size_t> _offset;
40
 
        size_t _count;
41
 
        T _data[C];
42
 
    } __attribute__ ((aligned (64)));
43
 
    
44
 
    struct index_t
45
 
    {
46
 
        bucket_t* _index[C];
47
 
        std::atomic<index_t*> _next;
48
 
    };
49
 
 
50
 
    bucket_t* _begin;
51
 
    std::vector<bucket_t* > _tnext;
52
 
    index_t* _index;
53
 
public:
54
 
 
55
 
    linked_bucket_t(size_t threads)
56
 
    : _tnext(threads) {
57
 
        for (size_t i = 0; i < threads; ++i) {
58
 
            _tnext[i] = NULL;
59
 
        }
60
 
        _begin = new bucket_t;
61
 
        _begin->_count = 0;
62
 
        _begin->_offset = 0;
63
 
        _begin->_nbucket = NULL;
64
 
        _tnext[0] = _begin;
65
 
 
66
 
        _index = new index_t;
67
 
        _index->_next = NULL;
68
 
 
69
 
        memset(&_begin->_data, 0, sizeof(T)*C);        
70
 
        memset(&_index->_index, 0, sizeof(bucket_t*)*C);
71
 
        _index->_index[0] = _begin;
72
 
    }
73
 
 
74
 
    virtual ~linked_bucket_t() {
75
 
 
76
 
        do {
77
 
            bucket_t* n = _begin->_nbucket.load();
78
 
            delete _begin;
79
 
            _begin = n;
80
 
 
81
 
        } while (_begin != NULL);
82
 
 
83
 
        do {
84
 
            index_t* n = _index->_next.load();
85
 
            delete _index;
86
 
            _index = n;
87
 
 
88
 
        } while (_index != NULL);
89
 
    }
90
 
 
91
 
    inline T& operator[](size_t i) {
92
 
        bucket_t* n = indexToBucket(i);
93
 
        if(n != NULL)
94
 
        {
95
 
            return n->_data[i % C];
96
 
        }
97
 
        
98
 
        size_t b = C;
99
 
        n = _begin;
100
 
        while (b <= i) {
101
 
            b += C;
102
 
            n = n->_nbucket.load();
103
 
            if(n == NULL) std::cerr << "FAILED FETCHING ID: " << i << std::endl;
104
 
            assert(n != NULL);
105
 
        }
106
 
 
107
 
        return n->_data[i % C];
108
 
    }
109
 
 
110
 
    inline const T& operator[](size_t i) const {
111
 
 
112
 
        bucket_t* n = indexToBucket(i);
113
 
        if(n != NULL)
114
 
        {
115
 
            return n->_data[i % C];
116
 
        }
117
 
        
118
 
        n = _begin;        
119
 
        size_t b = C;
120
 
 
121
 
        while (b <= i) {
122
 
            b += C;
123
 
            n = n->_nbucket.load();
124
 
            assert(n != NULL);
125
 
        }
126
 
 
127
 
        return n->_data[i % C];
128
 
    }
129
 
 
130
 
    size_t size() {
131
 
        bucket_t* n = _begin;
132
 
        size_t cnt = 0;
133
 
        while (n != NULL) {
134
 
            cnt += n->_count;
135
 
            n = n->_nbucket.load();
136
 
        }
137
 
        return cnt;
138
 
    }
139
 
 
140
 
    inline size_t next(size_t thread) {
141
 
        if (_tnext[thread] == NULL || _tnext[thread]->_count == C) {
142
 
            bucket_t* next = new bucket_t;
143
 
            next->_count = 0;
144
 
            next->_nbucket = NULL;
145
 
            next->_offset = 0;
146
 
            memset(&next->_data, 0, sizeof(T)*C);
147
 
            
148
 
            bucket_t* n = _tnext[thread];
149
 
            if (n == NULL) {
150
 
                n = _begin;
151
 
            }
152
 
 
153
 
            next->_offset = n->_offset.load() + C; // beginning of next
154
 
 
155
 
            bucket_t* tmp = NULL;
156
 
 
157
 
            while (!n->_nbucket.compare_exchange_weak(tmp, next)) {
158
 
                if (tmp != NULL) {
159
 
                    assert(tmp != NULL);
160
 
                    n = tmp;
161
 
                    next->_offset += C;
162
 
                }
163
 
            }
164
 
            _tnext[thread] = next;
165
 
 
166
 
            insertToIndex(next, next->_offset);            
167
 
        }
168
 
 
169
 
        bucket_t* c = _tnext[thread];
170
 
 
171
 
        // return old counter value, then increment
172
 
        return c->_offset + (c->_count++);
173
 
    }
174
 
    
175
 
    private:
176
 
        
177
 
        inline void insertToIndex(bucket_t* bucket, size_t id)
178
 
        {
179
 
            index_t* tmp = _index;
180
 
            while(id >= C*C)
181
 
            {
182
 
                index_t* old = tmp;
183
 
                tmp = old->_next;
184
 
                if(tmp == NULL)
185
 
                {
186
 
                    // extend index if needed
187
 
                    index_t* nindex = new index_t;
188
 
                    memset(&nindex->_index, 0, sizeof(bucket_t*)*C);
189
 
                    nindex->_next = 0;
190
 
                    if(!old->_next.compare_exchange_strong(tmp, nindex)) 
191
 
                    {
192
 
                        delete nindex;
193
 
                        tmp = old;
194
 
                        continue;
195
 
                    }
196
 
                    else
197
 
                    {
198
 
                        tmp = nindex;
199
 
                    }
200
 
                }
201
 
                id -= C*C;
202
 
            }
203
 
            tmp->_index[id/C] = bucket;
204
 
        }
205
 
        
206
 
        inline bucket_t* indexToBucket(size_t id)
207
 
        {
208
 
            index_t* tmp = _index;
209
 
            while(id >= C*C)
210
 
            {
211
 
                tmp = tmp->_next;
212
 
                if(tmp == NULL) return NULL;
213
 
                id -= C*C;
214
 
            }
215
 
            return tmp->_index[id/C];
216
 
        }
217
 
} __attribute__ ((aligned (64)));
218
 
 
219
 
 
220
 
#endif /* LINKED_BUCKET_H */
221