1+
2+ #include " ../SharedVerifier/SharedVerifier.hpp"
3+ #include " LibOMPVerifier.hpp"
4+
5+
6+ // Recursive helper for getLayerAndDepthMapsSerial
7+ // Returns the depth of a node id, in a proof p, using and modifying
8+ // a global depth map for the proof.
9+ size_t getNodeDepthBF (const Proof& p, VertId id, DepthMap& depthMap){
10+ // Base case 1, we already know the depth of the node
11+ DepthMap::const_iterator depthMapIter = depthMap.find (id);
12+ if (depthMapIter != depthMap.end ()){
13+ return depthMapIter->second ;
14+ }
15+ // Base case 2, we're an assumption
16+ std::unordered_set<VertId> parents = p.nodeLookup .at (id).parents ;
17+ if (parents.size () == 0 ){
18+ depthMap[id] = 0 ;
19+ return 0 ;
20+ }
21+
22+ // Recursive case
23+ std::unordered_set<int >::const_iterator itr = parents.begin ();
24+ size_t maxDepth = getNodeDepthBF (p, *itr, depthMap);
25+ itr++;
26+ for (;itr != parents.end (); itr++){
27+ size_t curDepth = getNodeDepthBF (p, *itr, depthMap);
28+ if (curDepth > maxDepth){
29+ maxDepth = curDepth;
30+ }
31+ }
32+ depthMap[id] = maxDepth + 1 ;
33+ return maxDepth + 1 ;
34+ }
35+
36+ using FastLayerMap = std::vector<std::vector<VertId>>;
37+ using NodeVec = std::vector<VertId>;
38+ // O(n) serial construction of the depth and layer maps for a proof.
39+ // n is the number of nodes in the proof
40+ std::pair<FastLayerMap, NodeVec> getLayerMapBF (const Proof& p){
41+ // Depthmap construction is O(n) via dynamic programming
42+ DepthMap depthMap;
43+ NodeVec allNodes;
44+ allNodes.reserve (p.nodeLookup .size ());
45+ size_t maxDepth = 0 ;
46+ for (const auto & [id, node] : p.nodeLookup ){
47+ size_t curDepth = getNodeDepthBF (p, id, depthMap);
48+ allNodes.push_back (id);
49+ if (curDepth > maxDepth){
50+ maxDepth = curDepth;
51+ }
52+ }
53+
54+ // LayerMap construction O(n)
55+ // std::list fill constructor
56+ FastLayerMap layerVector (maxDepth + 1 , std::vector<VertId>());
57+ for (const auto & [id, depth] : depthMap){
58+ layerVector[depth].push_back (id);
59+ }
60+
61+ return std::make_pair (layerVector, allNodes);
62+ }
63+
64+ bool OMPVerifier::OMPVerifyBF (const Proof& p){
65+
66+ // Compute Layers in Serial
67+ auto [layerMap, allNodes] = getLayerMapBF (p);
68+
69+ bool result = true ;
70+ #pragma omp parallel for reduction (&&:result)
71+ for (int i = 0 ; i < allNodes.size (); i++){
72+ result = SharedVerifier::verifyVertexSyntax (p, allNodes[i]);
73+ }
74+ if (!result) {
75+ return false ;
76+ }
77+
78+ Assumptions assumptions;
79+ for (size_t j = 0 ; j < layerMap.size (); j++){
80+ std::vector<VertId> layer = layerMap[j];
81+
82+ #ifdef PRINT_DEBUG
83+ std::cout<< " Layer " " Assumptions "
84+ SharedVerifier::assumptionsToString (assumptions) << std::endl;
85+ #endif
86+
87+ // Thread-safe data structures
88+ std::vector<std::unordered_set<VertId>> resultAssumptions (layer.size (), std::unordered_set<VertId>());
89+
90+ // Parallel Reduction
91+ #pragma omp parallel for reduction (&&:result)
92+ for (size_t i = 0 ; i < layer.size (); i++){
93+ result = SharedVerifier::verifyVertexSemantics (p, layer[i], assumptions, resultAssumptions[i]);
94+ }
95+
96+ if (!result) {
97+ return false ;
98+ }
99+
100+ #ifdef PRINT_DEBUG
101+ std::cout<<" Result Assumptions: "
102+ for (size_t i = 0 ; i < layer.size (); i++){
103+ std::cout<<layer[i]<<" :("
104+ for (VertId assumpt : resultAssumptions[i]){
105+ std::cout<<assumpt<<" ,"
106+ }
107+ std::cout<<" \b ),"
108+ }
109+ std::cout<<" \b "
110+ #endif
111+ // Update assumptions for each node we just verified
112+ for (size_t i = 0 ; i < layer.size (); i++){
113+ assumptions[layer[i]] = std::move (resultAssumptions[i]);
114+ }
115+ }
116+ return true ;
117+ }
0 commit comments