← Back to branch summary

~tapaal-ltl/verifypn/scc-optimise

« back to all changes in this revision

Viewing changes to include/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:
include/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] = nullptr;
 
59
        }
 
60
        _begin = new bucket_t;
 
61
        _begin->_count = 0;
 
62
        _begin->_offset = 0;
 
63
        _begin->_nbucket = nullptr;
 
64
        _tnext[0] = _begin;
 
65
 
 
66
        _index = new index_t;
 
67
        _index->_next = nullptr;
 
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
    ~linked_bucket_t() {
 
75
 
 
76
        do {
 
77
            bucket_t* n = _begin->_nbucket.load();
 
78
            delete _begin;
 
79
            _begin = n;
 
80
 
 
81
        } while (_begin != nullptr);
 
82
 
 
83
        do {
 
84
            index_t* n = _index->_next.load();
 
85
            delete _index;
 
86
            _index = n;
 
87
 
 
88
        } while (_index != nullptr);
 
89
    }
 
90
 
 
91
    inline T& operator[](size_t i) {
 
92
        bucket_t* n = indexToBucket(i);
 
93
        if(n != nullptr)
 
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 == nullptr) std::cerr << "FAILED FETCHING ID: " << i << std::endl;
 
104
            assert(n != nullptr);
 
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 != nullptr)
 
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 != nullptr);
 
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 != nullptr) {
 
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] == nullptr || _tnext[thread]->_count == C) {
 
142
            bucket_t* next = new bucket_t;
 
143
            next->_count = 0;
 
144
            next->_nbucket = nullptr;
 
145
            next->_offset = 0;
 
146
            memset(&next->_data, 0, sizeof(T)*C);
 
147
            
 
148
            bucket_t* n = _tnext[thread];
 
149
            if (n == nullptr) {
 
150
                n = _begin;
 
151
            }
 
152
 
 
153
            next->_offset = n->_offset.load() + C; // beginning of next
 
154
 
 
155
            bucket_t* tmp = nullptr;
 
156
 
 
157
            while (!n->_nbucket.compare_exchange_weak(tmp, next)) {
 
158
                if (tmp != nullptr) {
 
159
                    assert(tmp != nullptr);
 
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
    inline void pop_back(size_t thread)
 
176
    {
 
177
        assert(_tnext[thread] != nullptr && _tnext[thread]->_count > 0);
 
178
        --_tnext[thread]->_count;
 
179
    }
 
180
    
 
181
    private:
 
182
        
 
183
        inline void insertToIndex(bucket_t* bucket, size_t id)
 
184
        {
 
185
            index_t* tmp = _index;
 
186
            while(id >= C*C)
 
187
            {
 
188
                index_t* old = tmp;
 
189
                tmp = old->_next;
 
190
                if(tmp == nullptr)
 
191
                {
 
192
                    // extend index if needed
 
193
                    index_t* nindex = new index_t;
 
194
                    memset(&nindex->_index, 0, sizeof(bucket_t*)*C);
 
195
                    nindex->_next = 0;
 
196
                    if(!old->_next.compare_exchange_strong(tmp, nindex)) 
 
197
                    {
 
198
                        delete nindex;
 
199
                        tmp = old;
 
200
                        continue;
 
201
                    }
 
202
                    else
 
203
                    {
 
204
                        tmp = nindex;
 
205
                    }
 
206
                }
 
207
                id -= C*C;
 
208
            }
 
209
            tmp->_index[id/C] = bucket;
 
210
        }
 
211
        
 
212
        inline bucket_t* indexToBucket(size_t id)
 
213
        {
 
214
            index_t* tmp = _index;
 
215
            while(id >= C*C)
 
216
            {
 
217
                tmp = tmp->_next;
 
218
                if(tmp == nullptr) return nullptr;
 
219
                id -= C*C;
 
220
            }
 
221
            return tmp->_index[id/C];
 
222
        }
 
223
} __attribute__ ((aligned (64)));
 
224
 
 
225
 
 
226
#endif /* LINKED_BUCKET_H */
 
227