@@ -15,12 +15,6 @@ bool OMPVerifier::OMPVerifyLB(const Proof& p){
15
15
layers.push_back (std::vector<VertId>(layer.begin (), layer.end ()));
16
16
}
17
17
18
- // // Related to trying to get OpenMP to figure it out
19
- // std::vector<VertId> nodes(p.nodeLookup.size());
20
- // for (const auto &[id, node] : p.nodeLookup) {
21
- // nodes.push_back(id);
22
- // }
23
-
24
18
// Keep track of nodes that were syntax checked
25
19
std::unordered_map<VertId, bool > syntaxChecked (p.nodeLookup .size ());
26
20
for (const auto &[vertId, node] : p.nodeLookup ) {
@@ -32,88 +26,146 @@ bool OMPVerifier::OMPVerifyLB(const Proof& p){
32
26
for (size_t j = 0 ; j < layerMap.size (); j++){
33
27
const std::vector<VertId>& layer = layers[j];
34
28
35
- std::optional<std::vector<VertId>> nextLayer;
36
- if (j < layerMap.size () - 1 ) {
37
- nextLayer = layers[j + 1 ];
38
- }
29
+ const bool nextLayerExists = j < layerMap.size () - 1 ;
30
+ const size_t nextLayerSize = (nextLayerExists)? layers[j + 1 ].size () : 0 ;
31
+
39
32
40
33
#ifdef PRINT_DEBUG
41
34
std::cout<< " Layer " <<j<<" Assumptions " << \
42
35
SharedVerifier::assumptionsToString (assumptions) << std::endl;
43
36
#endif
44
37
38
+ // Thread safe data structures
45
39
bool result = true ;
46
40
std::vector<std::unordered_set<VertId>> resultAssumptions (layer.size (), std::unordered_set<VertId>());
47
- size_t nextLayerSize = (nextLayer.has_value ())? nextLayer.value ().size () : 0 ;
48
41
std::vector<VertId> resultSyntaxCheck (layer.size () + nextLayerSize);
42
+
43
+ // Setup thread counts
44
+ size_t num_threads;
45
+ bool envSet = std::sscanf (
46
+ std::getenv (" OMP_NUM_THREADS" ),
47
+ " %zu" , &num_threads
48
+ );
49
+ if (!envSet) {
50
+ throw std::runtime_error (" Need to set OMP_NUM_THREADS" );
51
+ }
52
+
53
+
54
+ const size_t leftOvers = layer.size () % num_threads;
55
+ const size_t elementsPerThread = layer.size () / num_threads;
56
+ const size_t lastNameBetter = num_threads * elementsPerThread;
57
+
58
+ // std::cout << "Layer Size: " << layer.size() << std::endl;
59
+ // std::cout << "Next Layer Size: " << nextLayerSize << std::endl;
60
+ // std::cout << "Number Threads: " << num_threads << std::endl;
61
+
62
+ // std::cout << "Layer: ";
63
+ // for (auto vertId : layer) {
64
+ // std::cout << vertId << ", ";
65
+ // }
66
+ // std::cout << std::endl;
67
+
68
+
69
+ omp_set_dynamic (0 );
70
+ omp_set_num_threads (num_threads);
49
71
#pragma omp parallel reduction(&&:result)
50
72
{
51
- size_t thread_id = omp_get_thread_num ();
52
- size_t num_threads = omp_get_num_threads ();
73
+ const size_t thread_id = omp_get_thread_num ();
74
+ const size_t start = thread_id * elementsPerThread;
75
+ const size_t end = (thread_id + 1 ) * elementsPerThread;
53
76
54
- size_t elementsPerThread = layer.size () / num_threads;
55
- size_t start = thread_id * elementsPerThread;
56
- size_t end = (thread_id + 1 ) * elementsPerThread;
57
-
58
- for (size_t i = start; i < end; ++i) {
77
+ for (size_t i = start; i < end; i++) {
59
78
if (syntaxChecked.at (layer[i])) {
79
+ // std::string toPrint3 = std::string("Already Syntax Checked: ");
80
+ // toPrint3 += std::to_string(layer[i]) += std::string("\n");
81
+ // std::cout << toPrint3;
82
+
60
83
// If we already verified the syntax, only check the semantics
61
84
result = SharedVerifier::verifyVertexSemantics (p, layer[i], assumptions, resultAssumptions[i]);
85
+
86
+ // std::string toPrint11 = std::string("Verified semantics of: ");
87
+ // toPrint11 += std::to_string(layer[i]) + std::string("\n");
88
+ // std::cout << toPrint11;
89
+
62
90
} else {
63
91
// Otherwise check both syntax and semantics
64
- // std::cout << "HUMANS 1\n"; // TODO: Why doesn't this trigger?
92
+
93
+ // std::string toPrint9 = std::string("Full Verifying Vertex: ") + std::to_string(layer[i]);
94
+ // toPrint9 += std::string("\n");
95
+ // std::cout << toPrint9;
96
+
65
97
result = SharedVerifier::verifyVertex (p, layer[i], assumptions, resultAssumptions[i]);
98
+
99
+
100
+ // std::string toPrint8 = std::string("Verified Fully Vertex: ") + std::to_string(layer[i]);
101
+ // toPrint8 += std::string(" Setting RSC[") + std::to_string(i);
102
+ // toPrint8 += std::string("] to true\n");
103
+ // std::cout << toPrint8;
104
+
66
105
resultSyntaxCheck[i] = true ;
106
+
107
+ // std::cout << "H3 Success\n";
67
108
}
68
109
}
69
110
70
- size_t leftOvers = layer.size () % num_threads;
111
+ // size_t leftOvers = layer.size() % num_threads;
112
+
113
+ // std::string toPrint0 = std::string("Layer Size: ") + std::to_string(layer.size());
114
+ // toPrint0 += std::string(" ElementsPerThread: ") + std::to_string(elementsPerThread);
115
+ // toPrint0 += std::string(" Leftovers: ") + std::to_string(leftOvers);
116
+ // toPrint0 += std::string(" ForwardCheck: ") + std::to_string(num_threads - leftOvers);
117
+ // toPrint0 += std::string("\n");
118
+ // std::cout << toPrint0;
119
+
71
120
if (thread_id < leftOvers) {
72
121
// Each thread will verify one of the nodes left
73
122
// on this layer.
74
- result = SharedVerifier::verifyVertex (p, layer[end + thread_id], assumptions, resultAssumptions[end + thread_id]);
75
- resultSyntaxCheck[end + thread_id] = true ;
123
+ // std::string toPrint12 = std::string("Verifying LeftOver: ");
124
+ // toPrint12 += std::to_string(layer[lastNameBetter + thread_id]) + std::string("\n");
125
+ // std::cout << toPrint12;
76
126
77
- } else if (nextLayer.has_value ()) {
127
+ if (syntaxChecked.at (lastNameBetter + thread_id)) {
128
+ result = SharedVerifier::verifyVertexSemantics (p, layer[lastNameBetter + thread_id], assumptions, resultAssumptions[lastNameBetter + thread_id]);
129
+ } else {
130
+ result = SharedVerifier::verifyVertex (p, layer[lastNameBetter + thread_id], assumptions, resultAssumptions[lastNameBetter + thread_id]);
131
+ }
132
+
133
+ // std::string toPrint5 = std::string("Verified Leftover: ") + std::to_string(layer[lastNameBetter + thread_id]);
134
+ // toPrint5 += std::string(" Setting RSC[") + std::to_string(lastNameBetter + thread_id);
135
+ // toPrint5 += std::string("] to true\n");
136
+ // std::cout << toPrint5;
137
+
138
+ resultSyntaxCheck[lastNameBetter + thread_id] = true ;
139
+
140
+ // std::cout << "H1 Success\n";
141
+ } else if (nextLayerExists) {
78
142
// These threads will look ahead to the next layer and
79
143
// verify a syntax.
80
144
size_t newIndex = (thread_id - leftOvers);
81
- if (newIndex < nextLayer.value ().size ()) {
82
- /*
83
- Current Layer Size: 2 Next Layer Size: 1 newIndex: 0 vertId: 3
84
- Current Layer Size: 1 Next Layer Size: 1 newIndex: 0 vertId: 21941
85
- terminate called after throwing an instance of 'std::out_of_range'
86
- what(): _Map_base::at
87
- Aborted (core dumped)
88
- Note: the vertId is super high for some reason
89
- */
90
- // VertId nodeId = (nextLayer.value())[thread_id];
91
- // std::string toPrint = std::string("Current Layer Size: ") + std::to_string(layer.size());
92
- // toPrint += std::string(" Next Layer Size: ") + std::to_string(nextLayer.value().size());
93
- // toPrint += " newIndex: " + std::to_string(newIndex);
94
- // toPrint += " vertId: " + std::to_string(nodeId) + std::string("\n");
145
+ if (newIndex < layers[j + 1 ].size ()) {
146
+ VertId nodeId = layers[j + 1 ].at (newIndex);
147
+
148
+ // std::string toPrint = std::string("Forward Checking: ");
149
+ // toPrint += std::to_string(nodeId) + std::string("\n");
95
150
// std::cout << toPrint;
96
- // result = SharedVerifier::verifyVertexSyntax(p, nodeId);
97
- // resultSyntaxCheck[layer.size() + newIndex] = true;
151
+
152
+
153
+ result = SharedVerifier::verifyVertexSyntax (p, nodeId);
154
+
155
+ // std::string toPrint7 = std::string("Verified FC: ") + std::to_string(nodeId);
156
+ // toPrint7 += std::string(" Setting RSC[") + std::to_string(layer.size() + newIndex);
157
+ // toPrint7 += std::string("] to true\n");
158
+ // std::cout << toPrint7;
159
+
160
+ resultSyntaxCheck[layer.size () + newIndex] = true ;
161
+ // std::cout << "H2 Success\n";
98
162
}
99
163
100
164
}
101
165
102
166
} // End parallel block
103
- // std::cout << std::endl;
167
+
104
168
105
- // // Attempt to let OpenMP figure it out, doesn't work sadly
106
- // #pragma omp parallel
107
- // {
108
- // #pragma omp for reduction(&&:result)
109
- // for(size_t i = 0; i < layer.size(); i++){
110
- // result = SharedVerifier::verifyVertexSemantics(p, layer[i], assumptions, resultAssumptions[i]);
111
- // }
112
- // #pragma omp for reduction(&&:syntaxResult)
113
- // for(size_t i = 0; i < nodes.size(); i++){
114
- // syntaxResult = SharedVerifier::verifyVertexSyntax(p, nodes[i]);
115
- // }
116
- // }
117
169
if (!result) {
118
170
return false ;
119
171
}
@@ -136,14 +188,23 @@ bool OMPVerifier::OMPVerifyLB(const Proof& p){
136
188
}
137
189
138
190
// Update syntax checked
139
- // for (size_t i = 0; i < layer.size(); i++) {
140
- // syntaxChecked[layer[i]] = resultSyntaxCheck[i];
141
- // }
142
- // if (nextLayerExists) {
143
- // for (size_t i = 0; i < nextLayerSize; i++) {
144
- // syntaxChecked[nextLayer[i]] = resultSyntaxCheck[layer.size() + i];
145
- // }
146
- // }
191
+ // std::cout << "Current Layer RSC copy" << std::endl;
192
+ for (size_t i = 0 ; i < layer.size (); i++) {
193
+ syntaxChecked[layer[i]] = resultSyntaxCheck[i];
194
+ }
195
+ // std::cout << "Finished copy" << std::endl;
196
+
197
+ if (nextLayerExists) {
198
+ // std::cout << "currentLayer size: " << layer.size() << std::endl;
199
+ // std::cout << "nextLayer size: " << nextLayer.value().size() << std::endl;
200
+ // std::cout << "RSC size: " << resultSyntaxCheck.size() << std::endl;
201
+ for (size_t i = 0 ; i < (num_threads - leftOvers) && i < layers[j + 1 ].size (); i++) {
202
+ // std::cout << "Inner: " << layer.size() + i << std::endl;
203
+ syntaxChecked[layers[j + 1 ].at (i)] = resultSyntaxCheck[layer.size () + i];
204
+ }
205
+ }
206
+
207
+ // std::cout << std::endl; // Space between each layer
147
208
148
209
149
210
}
0 commit comments