socialg.it will shutdown on the 8th of February 2021 in favour of a new Git hosting system (Gitea) at git.socialnerds.org. Read the blog post.

Commit 94a1cb96 authored by phlo's avatar phlo

updated FENCE to mark next instruction as barrier

parent b8314541
......@@ -21,7 +21,9 @@
// constructors
//------------------------------------------------------------------------------
Program::Program(std::istream & f, const std::string & p) : path(p)
Program::Program(std::istream & f, const std::string & p) :
path(p),
set_memory_barrier(false)
{
std::string token;
......@@ -206,30 +208,24 @@ Program::Program(std::istream & f, const std::string & p) : path(p)
void Program::push_back (Instruction && op)
{
// assign checkpoint
// collect checkpoint id
if (&op.symbol() == &Instruction::Check::symbol)
{
// collect checkpoint id
checkpoints[op.arg()].push_back(size());
// set the following instruction's type
set_type = set_type.value_or(0) | op.type();
checkpoints[op.arg()].push_back(size());
// return;
}
// assign memory barrier
// define the following instruction as memory barrier
if (&op.symbol() == &Instruction::Fence::symbol)
{
// set the following instruction's type
set_type = set_type.value_or(0) | op.type() | Instruction::Type::barrier;
set_memory_barrier = true;
// return;
return;
}
// define instruction as checkpoint or memory barrier
if (set_type)
if (set_memory_barrier)
{
op.type(op.type() | Instruction::Type::barrier);
set_memory_barrier = false;
}
// append instruction
......
......@@ -67,9 +67,9 @@ struct Program : public std::vector<Instruction>
//
std::unordered_set<std::string> labels;
// next instruction's type
// define next instruction as memory barrier
//
std::optional<uint8_t> set_type;
bool set_memory_barrier;
//----------------------------------------------------------------------------
// constructors
......
This source diff could not be displayed because it is too large. You can view the blob instead.
......@@ -15,7 +15,7 @@
6 zero 2
7 one 2
8 constd 2 3
8 constd 2 2
9 constd 2 16
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
......@@ -49,281 +49,267 @@
23 state 1 stmt_0_3
24 state 1 stmt_0_4
25 state 1 stmt_0_5
26 state 1 stmt_0_6
27 state 1 stmt_1_0
28 state 1 stmt_1_1
29 state 1 stmt_1_2
30 state 1 stmt_1_3
31 state 1 stmt_1_4
32 state 1 stmt_1_5
33 state 1 stmt_1_6
26 state 1 stmt_1_0
27 state 1 stmt_1_1
28 state 1 stmt_1_2
29 state 1 stmt_1_3
30 state 1 stmt_1_4
31 state 1 stmt_1_5
; blocking variables - block_<id>_<thread>
34 state 1 block_0_0
35 state 1 block_0_1
32 state 1 block_0_0
33 state 1 block_0_1
; heap variable
36 state 3 heap
34 state 3 heap
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; input variable declarations
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; thread activation variables - thread_<thread>
37 input 1 thread_0
38 input 1 thread_1
35 input 1 thread_0
36 input 1 thread_1
; store buffer flush variables - flush_<thread>
39 input 1 flush_0
40 input 1 flush_1
37 input 1 flush_0
38 input 1 flush_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; transition variable definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; statement execution variables - exec_<thread>_<pc>
41 and 1 20 37 exec_0_0
42 and 1 21 37 exec_0_1
43 and 1 22 37 exec_0_2
44 and 1 23 37 exec_0_3
45 and 1 24 37 exec_0_4
46 and 1 25 37 exec_0_5
47 and 1 26 37 exec_0_6
48 and 1 27 38 exec_1_0
49 and 1 28 38 exec_1_1
50 and 1 29 38 exec_1_2
51 and 1 30 38 exec_1_3
52 and 1 31 38 exec_1_4
53 and 1 32 38 exec_1_5
54 and 1 33 38 exec_1_6
39 and 1 20 35 exec_0_0
40 and 1 21 35 exec_0_1
41 and 1 22 35 exec_0_2
42 and 1 23 35 exec_0_3
43 and 1 24 35 exec_0_4
44 and 1 25 35 exec_0_5
45 and 1 26 36 exec_1_0
46 and 1 27 36 exec_1_1
47 and 1 28 36 exec_1_2
48 and 1 29 36 exec_1_3
49 and 1 30 36 exec_1_4
50 and 1 31 36 exec_1_5
; checkpoint variables - check_<id>
55 and 1 34 35 check_0
51 and 1 32 33 check_0
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; state variable definitions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; accu variables - accu_<thread>
56 init 2 10 6
57 read 2 36 6
58 eq 1 14 6
59 and 1 18 58
60 ite 2 59 16 57
61 ite 2 44 60 10 0:3:MEM:0
62 add 2 10 7
63 ite 2 45 62 61 0:4:ADDI:1
64 eq 1 12 60
65 ite 2 64 7 6
66 ite 2 46 65 63 0:5:CAS:0
67 next 2 10 66 accu_0
68 init 2 11 6
69 eq 1 15 6
70 and 1 19 69
71 ite 2 70 17 57
72 ite 2 51 71 11 1:3:MEM:0
73 add 2 11 7
74 ite 2 52 73 72 1:4:ADDI:1
75 eq 1 13 71
76 ite 2 75 7 6
77 ite 2 53 76 74 1:5:CAS:0
78 next 2 11 77 accu_1
52 init 2 10 6
53 read 2 34 6
54 eq 1 14 6
55 and 1 18 54
56 ite 2 55 16 53
57 ite 2 41 56 10 0:2:MEM:0
58 add 2 10 7
59 ite 2 42 58 57 0:3:ADDI:1
60 eq 1 12 56
61 ite 2 60 7 6
62 ite 2 43 61 59 0:4:CAS:0
63 next 2 10 62 accu_0
64 init 2 11 6
65 eq 1 15 6
66 and 1 19 65
67 ite 2 66 17 53
68 ite 2 47 67 11 1:2:MEM:0
69 add 2 11 7
70 ite 2 48 69 68 1:3:ADDI:1
71 eq 1 13 67
72 ite 2 71 7 6
73 ite 2 49 72 70 1:4:CAS:0
74 next 2 11 73 accu_1
; mem variables - mem_<thread>
79 init 2 12 6
80 ite 2 44 60 12 0:3:MEM:0
81 next 2 12 80 mem_0
75 init 2 12 6
76 ite 2 41 56 12 0:2:MEM:0
77 next 2 12 76 mem_0
82 init 2 13 6
83 ite 2 51 71 13 1:3:MEM:0
84 next 2 13 83 mem_1
78 init 2 13 6
79 ite 2 47 67 13 1:2:MEM:0
80 next 2 13 79 mem_1
; store buffer address variables - sb-adr_<thread>
85 init 2 14 6
86 ite 2 41 6 14 0:0:STORE:0
87 next 2 14 86 sb-adr_0
81 init 2 14 6
82 ite 2 39 6 14 0:0:STORE:0
83 next 2 14 82 sb-adr_0
88 init 2 15 6
89 ite 2 48 6 15 1:0:STORE:0
90 next 2 15 89 sb-adr_1
84 init 2 15 6
85 ite 2 45 6 15 1:0:STORE:0
86 next 2 15 85 sb-adr_1
; store buffer value variables - sb-val_<thread>
91 init 2 16 6
92 ite 2 41 10 16 0:0:STORE:0
93 next 2 16 92 sb-val_0
87 init 2 16 6
88 ite 2 39 10 16 0:0:STORE:0
89 next 2 16 88 sb-val_0
94 init 2 17 6
95 ite 2 48 11 17 1:0:STORE:0
96 next 2 17 95 sb-val_1
90 init 2 17 6
91 ite 2 45 11 17 1:0:STORE:0
92 next 2 17 91 sb-val_1
; store buffer full variables - sb-full_<thread>
97 init 1 18 4
98 or 1 41 18
99 ite 1 39 4 98
100 next 1 18 99 sb-full_0
93 init 1 18 4
94 or 1 39 18
95 ite 1 37 4 94
96 next 1 18 95 sb-full_0
101 init 1 19 4
102 or 1 48 19
103 ite 1 40 4 102
104 next 1 19 103 sb-full_1
97 init 1 19 4
98 or 1 45 19
99 ite 1 38 4 98
100 next 1 19 99 sb-full_1
; statement activation variables - stmt_<thread>_<pc>
105 init 1 20 5
106 and 1 20 -41 0:0:STORE:0
107 next 1 20 106 stmt_0_0
108 init 1 21 4
109 and 1 21 -42 0:1:FENCE
110 ite 1 20 41 109 0:0:STORE:0
111 next 1 21 110 stmt_0_1
112 init 1 22 4
113 and 1 22 -43 0:2:CHECK:0
114 ite 1 21 42 113 0:1:FENCE
115 next 1 22 114 stmt_0_2
116 init 1 23 4
117 and 1 23 -44 0:3:MEM:0
118 ite 1 22 43 117 0:2:CHECK:0
119 ite 1 26 47 118 0:6:JMP:3
120 next 1 23 119 stmt_0_3
121 init 1 24 4
122 and 1 24 -45 0:4:ADDI:1
123 ite 1 23 44 122 0:3:MEM:0
124 next 1 24 123 stmt_0_4
125 init 1 25 4
126 and 1 25 -46 0:5:CAS:0
127 ite 1 24 45 126 0:4:ADDI:1
128 next 1 25 127 stmt_0_5
129 init 1 26 4
130 and 1 26 -47 0:6:JMP:3
131 ite 1 25 46 130 0:5:CAS:0
132 next 1 26 131 stmt_0_6
133 init 1 27 5
134 and 1 27 -48 1:0:STORE:0
135 next 1 27 134 stmt_1_0
136 init 1 28 4
137 and 1 28 -49 1:1:FENCE
138 ite 1 27 48 137 1:0:STORE:0
139 next 1 28 138 stmt_1_1
140 init 1 29 4
141 and 1 29 -50 1:2:CHECK:0
142 ite 1 28 49 141 1:1:FENCE
143 next 1 29 142 stmt_1_2
144 init 1 30 4
145 and 1 30 -51 1:3:MEM:0
146 ite 1 29 50 145 1:2:CHECK:0
147 ite 1 33 54 146 1:6:JMP:3
148 next 1 30 147 stmt_1_3
149 init 1 31 4
150 and 1 31 -52 1:4:ADDI:1
151 ite 1 30 51 150 1:3:MEM:0
152 next 1 31 151 stmt_1_4
153 init 1 32 4
154 and 1 32 -53 1:5:CAS:0
155 ite 1 31 52 154 1:4:ADDI:1
156 next 1 32 155 stmt_1_5
157 init 1 33 4
158 and 1 33 -54 1:6:JMP:3
159 ite 1 32 53 158 1:5:CAS:0
160 next 1 33 159 stmt_1_6
101 init 1 20 5
102 and 1 20 -39 0:0:STORE:0
103 next 1 20 102 stmt_0_0
104 init 1 21 4
105 and 1 21 -40 0:1:CHECK:0
106 ite 1 20 39 105 0:0:STORE:0
107 next 1 21 106 stmt_0_1
108 init 1 22 4
109 and 1 22 -41 0:2:MEM:0
110 ite 1 21 40 109 0:1:CHECK:0
111 ite 1 25 44 110 0:5:JMP:2
112 next 1 22 111 stmt_0_2
113 init 1 23 4
114 and 1 23 -42 0:3:ADDI:1
115 ite 1 22 41 114 0:2:MEM:0
116 next 1 23 115 stmt_0_3
117 init 1 24 4
118 and 1 24 -43 0:4:CAS:0
119 ite 1 23 42 118 0:3:ADDI:1
120 next 1 24 119 stmt_0_4
121 init 1 25 4
122 and 1 25 -44 0:5:JMP:2
123 ite 1 24 43 122 0:4:CAS:0
124 next 1 25 123 stmt_0_5
125 init 1 26 5
126 and 1 26 -45 1:0:STORE:0
127 next 1 26 126 stmt_1_0
128 init 1 27 4
129 and 1 27 -46 1:1:CHECK:0
130 ite 1 26 45 129 1:0:STORE:0
131 next 1 27 130 stmt_1_1
132 init 1 28 4
133 and 1 28 -47 1:2:MEM:0
134 ite 1 27 46 133 1:1:CHECK:0
135 ite 1 31 50 134 1:5:JMP:2
136 next 1 28 135 stmt_1_2
137 init 1 29 4
138 and 1 29 -48 1:3:ADDI:1
139 ite 1 28 47 138 1:2:MEM:0
140 next 1 29 139 stmt_1_3
141 init 1 30 4
142 and 1 30 -49 1:4:CAS:0
143 ite 1 29 48 142 1:3:ADDI:1
144 next 1 30 143 stmt_1_4
145 init 1 31 4
146 and 1 31 -50 1:5:JMP:2
147 ite 1 30 49 146 1:4:CAS:0
148 next 1 31 147 stmt_1_5
; blocking variables - block_<id>_<thread>
161 init 1 34 4
162 or 1 43 34
163 ite 1 55 4 162
164 next 1 34 163 block_0_0
149 init 1 32 4
150 or 1 40 32
151 ite 1 51 4 150
152 next 1 32 151 block_0_0
165 init 1 35 4
166 or 1 50 35
167 ite 1 55 4 166
168 next 1 35 167 block_0_1
153 init 1 33 4
154 or 1 46 33
155 ite 1 51 4 154
156 next 1 33 155 block_0_1
; heap variable
169 write 3 36 14 16
170 ite 3 39 169 36 flush_0
171 write 3 36 6 10
172 ite 3 64 171 36
173 ite 3 46 172 170 0:5:CAS:0
174 write 3 36 15 17
175 ite 3 40 174 173 flush_1
176 write 3 36 6 11
177 ite 3 75 176 36
178 ite 3 53 177 175 1:5:CAS:0
179 next 3 36 178 heap
157 write 3 34 14 16
158 ite 3 37 157 34 flush_0
159 write 3 34 6 10
160 ite 3 60 159 34
161 ite 3 43 160 158 0:4:CAS:0
162 write 3 34 15 17
163 ite 3 38 162 161 flush_1
164 write 3 34 6 11
165 ite 3 71 164 34
166 ite 3 49 165 163 1:4:CAS:0
167 next 3 34 166 heap
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; scheduling constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
180 or 1 37 38
181 or 1 39 180
182 or 1 40 181
168 or 1 35 36
169 or 1 37 168
170 or 1 38 169
171 constraint 170
172 nand 1 35 36
173 nand 1 35 37
174 nand 1 35 38
175 nand 1 36 37
176 nand 1 36 38
177 nand 1 37 38
178 and 1 172 173
179 and 1 174 178
180 and 1 175 179
181 and 1 176 180
182 and 1 177 181
183 constraint 182
184 nand 1 37 38
185 nand 1 37 39
186 nand 1 37 40
187 nand 1 38 39
188 nand 1 38 40
189 nand 1 39 40
190 and 1 184 185
191 and 1 186 190
192 and 1 187 191
193 and 1 188 192
194 and 1 189 193
195 constraint 194
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; store buffer constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
196 or 1 20 21
197 or 1 25 196
198 implies 1 197 -37
199 ite 1 18 198 -39
200 constraint 199
184 or 1 20 21
185 or 1 24 184
186 implies 1 185 -35
187 ite 1 18 186 -37
188 constraint 187
201 or 1 27 28
202 or 1 32 201
203 implies 1 202 -38
204 ite 1 19 203 -40
205 constraint 204
189 or 1 26 27
190 or 1 30 189
191 implies 1 190 -36
192 ite 1 19 191 -38
193 constraint 192
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; checkpoint constraints
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
206 and 1 34 -55
207 implies 1 206 -37
208 constraint 207 block_0_0
194 and 1 32 -51
195 implies 1 194 -35
196 constraint 195 block_0_0
209 and 1 35 -55
210 implies 1 209 -38
211 constraint 210 block_0_1
197 and 1 33 -51
198 implies 1 197 -36
199 constraint 198 block_0_1
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; bound
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; step counter
212 state 2 k
213 init 2 212 6
214 add 2 7 212
215 next 2 212 214
200 state 2 k
201 init 2 200 6
202 add 2 7 200
203 next 2 200 202
; bound (16)
216 eq 1 9 212
217 bad 216
204 eq 1 9 200
205 bad 204
This diff is collapsed.
......@@ -52,8 +52,11 @@ TEST_F(Encoder, constructor_flush_pcs)
reset_encoder();
for (const auto & p : *encoder->programs)
ASSERT_EQ(2, p.size());
for (const auto & pcs : encoder->flush_pcs)
ASSERT_EQ(std::vector<word_t>({0, 1, 2}), pcs.second);
ASSERT_EQ(std::vector<word_t>({0, 1}), pcs.second);
}
TEST_F(Encoder, constructor_check_pcs)
......
......@@ -1405,15 +1405,15 @@ TEST_F(smtlib_Encoder, define_store_buffer_constraints)
"\n"
"(assert "
"(ite sb-full_1_0 "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2) (not thread_1_0)) "
"(=> (or stmt_1_0_0 stmt_1_0_1) (not thread_1_0)) "
"(not flush_1_0)))\n"
"(assert "
"(ite sb-full_1_1 "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2) (not thread_1_1)) "
"(=> (or stmt_1_1_0 stmt_1_1_1) (not thread_1_1)) "
"(not flush_1_1)))\n"
"(assert "
"(ite sb-full_1_2 "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2) (not thread_1_2)) "
"(=> (or stmt_1_2_0 stmt_1_2_1) (not thread_1_2)) "
"(not flush_1_2)))\n"
"\n",
encoder->str());
......@@ -1428,15 +1428,15 @@ TEST_F(smtlib_Encoder, define_store_buffer_constraints)
ASSERT_EQ(
"(assert "
"(ite sb-full_1_0 "
"(=> (or stmt_1_0_0 stmt_1_0_1 stmt_1_0_2) (not thread_1_0)) "
"(=> (or stmt_1_0_0 stmt_1_0_1) (not thread_1_0)) "
"(not flush_1_0)))\n"
"(assert "
"(ite sb-full_1_1 "
"(=> (or stmt_1_1_0 stmt_1_1_1 stmt_1_1_2) (not thread_1_1)) "
"(=> (or stmt_1_1_0 stmt_1_1_1) (not thread_1_1)) "
"(not flush_1_1)))\n"
"(assert "
"(ite sb-full_1_2 "
"(=> (or stmt_1_2_0 stmt_1_2_1 stmt_1_2_2) (not thread_1_2)) "
"(=> (or stmt_1_2_0 stmt_1_2_1) (not thread_1_2)) "
"(not flush_1_2)))\n"
"\n",
encoder->str());
......
......@@ -90,21 +90,20 @@ TEST_F(Program, parse)
{
program = create_from_file<::Program>("data/increment.cas.asm");
ASSERT_EQ(7, program.size());
ASSERT_EQ(6, program.size());
ASSERT_EQ(1, program.checkpoints.size());
ASSERT_EQ(1, program.labels.size());
ASSERT_EQ(1, program.pc_to_label.size());
ASSERT_EQ("LOOP", *program.pc_to_label[3]);
ASSERT_EQ("LOOP", *program.pc_to_label[2]);
ASSERT_EQ(1, program.label_to_pc.size());
ASSERT_EQ(3, program.label_to_pc[program.pc_to_label[3]]);
ASSERT_EQ(2, program.label_to_pc[program.pc_to_label[2]]);
ASSERT_EQ("0\tSTORE\t0", program.print(true, 0));
ASSERT_EQ("1\tFENCE\t", program.print(true, 1));
ASSERT_EQ("2\tCHECK\t0", program.print(true, 2));
ASSERT_EQ("LOOP\tMEM\t0", program.print(true, 3));
ASSERT_EQ("4\tADDI\t1", program.print(true, 4));
ASSERT_EQ("5\tCAS\t0", program.print(true, 5));
ASSERT_EQ("6\tJMP\tLOOP", program.print(true, 6));
ASSERT_EQ("1\tCHECK\t0", program.print(true, 1));
ASSERT_EQ("LOOP\tMEM\t0", program.print(true, 2));
ASSERT_EQ("3\tADDI\t1", program.print(true, 3));
ASSERT_EQ("4\tCAS\t0", program.print(true, 4));
ASSERT_EQ("5\tJMP\tLOOP", program.print(true, 5));
// indirect addressing
program = create_from_file<::Program>("data/indirect.addressing.asm");
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment