1\*************************************************************************** 2\* Copyright (c) 2021-2024 Huawei Device Co., Ltd. 3\* Licensed under the Apache License, Version 2.0 (the "License"); 4\* you may not use this file except in compliance with the License. 5\* You may obtain a copy of the License at 6\* 7\* http://www.apache.org/licenses/LICENSE-2.0 8\* 9\* Unless required by applicable law or agreed to in writing, software 10\* distributed under the License is distributed on an "AS IS" BASIS, 11\* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. 12\* See the License for the specific language governing permissions and 13\* limitations under the License. 14\*************************************************************************** 15 16---------------------------- MODULE thread_pool ---------------------------- 17EXTENDS Sequences, Integers, TLC 18 19CONSTANTS max_workers, max_producers, max_controllers, queue_max_size 20 21workers_set == 1..max_workers 22producers_set == (max_workers + 1)..(max_workers + max_producers) 23controllers_set == (max_workers + max_producers + 1)..(max_workers + max_producers + max_controllers) 24workers_initial_val == [i \in 1 .. max_workers |-> FALSE] 25 26(*--algorithm thread_pool 27 28variables workers = workers_initial_val, 29 workers_status = workers_initial_val, 30 num_workers = 0, 31 is_active = TRUE, 32 queue_lock_ = 0, 33 scale_lock_ = 0; 34 cond_var_ = FALSE; 35 queue_size_ = 0; 36 37\* Methods with return value 38 39define 40 is_full == queue_size_ >= queue_max_size 41end define; 42 43 44\* Synchronisation primitives 45macro lock(lock_var) 46begin 47 await lock_var = 0; 48 lock_var := self; 49end macro; 50 51macro unlock(lock_var) 52begin 53 assert (lock_var = self); 54 lock_var := 0; 55end macro; 56 57macro signal(cond_var) 58begin 59 cond_var := TRUE; 60end macro; 61 62macro wait_signal(lock_var, cond_var) 63begin 64 await cond_var = TRUE /\ lock_var = 0; 65 cond_var := FALSE || lock_var := self; 66end macro; 67 68macro join(worker_num) 69begin 70 await workers_status[worker_num] = FALSE; 71end macro; 72 73procedure timed_wait_signal() 74begin 75timed_wait_signal_entry: 76 either goto timed_wait_signal_wait; 77 or goto timed_wait_signal_exit; 78 end either; 79timed_wait_signal_wait: 80 unlock(queue_lock_); 81timed_wait_signal_wait_1: 82 if cond_var_ # TRUE \/ queue_lock_ # 0 then 83 if is_active = FALSE then 84 await queue_lock_ = 0; 85 queue_lock_ := self; 86 return; 87 else 88 goto timed_wait_signal_wait_1; 89 end if; 90 else 91 cond_var_ := FALSE || queue_lock_ := self; 92 end if; 93timed_wait_signal_exit: 94 return; 95end procedure; 96 97\* TaskQueueInterface methods 98 99procedure get_task() 100begin 101get_task_entry: 102 if queue_size_ = 0 then 103 task := 0; 104 else 105 task := 1; 106 queue_size_ := queue_size_ - 1; 107 end if; 108get_task_exit: 109 return; 110end procedure; 111 112procedure add_task() 113begin 114add_task_increase_queue_size: 115 queue_size_ := queue_size_ + 1; 116add_task_exit: 117 return; 118end procedure; 119 120procedure try_add_task() 121begin 122try_add_task_entry: 123 if is_full then 124 goto try_add_task_exit; 125 else 126try_add_task_increase_queue_size: 127 queue_size_ := queue_size_ + 1; 128 end if; 129try_add_task_exit: 130 return; 131end procedure; 132 133procedure finalize() 134begin 135finalize_entry: 136 queue_size_ := 0; 137finalize_exit: 138 return; 139end procedure; 140 141\* ThreadPool methods 142 143procedure stop_worker(worker_num) 144begin 145stop_worker_lock_and_signal: 146 lock(queue_lock_); 147stop_worker_finalize_queue: 148 call finalize(); 149stop_worker_unlock: 150 signal(cond_var_); 151 unlock(queue_lock_); 152stop_worker_join: 153 join(worker_num); 154 return; 155end procedure; 156 157procedure create_new_thread(worker_num) 158begin 159create_new_thread_lock: 160 lock(queue_lock_); 161 workers[num_workers + 1] := TRUE; 162create_new_thread_unlock: 163 unlock(queue_lock_); 164 return; 165end procedure; 166 167procedure scale(num) 168begin 169scale_lock: 170 lock(scale_lock_); 171 assert num \in 0..max_workers; 172scale_check: 173 if num > num_workers then goto scale_add_workers; 174 elsif num < num_workers then goto scale_del_workers; 175 else goto scale_ret; 176 end if; 177scale_add_workers: 178 while num_workers < num do 179 call create_new_thread(num_workers); 180scale_queue_inc_lock: 181 lock(queue_lock_); 182scale_add_workers_inc: 183 num_workers := num_workers + 1; 184scale_queue_inc_unlock: 185 unlock(queue_lock_); 186 end while; 187scale_del_workers: 188 while num_workers > num do 189 workers[num_workers] := FALSE; 190 call stop_worker(num_workers); 191scale_queue_dec_lock: 192 lock(queue_lock_); 193scale_del_workers_dec_num_workers: 194 num_workers := num_workers - 1; 195scale_queue_dec_unlock: 196 unlock(queue_lock_); 197 end while; 198scale_ret: 199 unlock(scale_lock_); 200 return 201end procedure; 202 203procedure enumerate_procs() 204begin 205enumerate_procs_lock: 206 lock(scale_lock_); 207enumerate_procs_unlock: 208 unlock(scale_lock_); 209 return 210end procedure; 211 212 213procedure shutdown() 214variable n = 1; 215begin 216shutdown_lock: 217 lock(scale_lock_); 218shutdown_loop: 219 while n <= num_workers do 220 call stop_worker(n); 221 shutdown_inc_n: 222 n := n + 1; 223 end while; 224shutdown_unlock: 225 unlock(scale_lock_); 226shutdown_exit: 227 return; 228end procedure; 229 230procedure wait_task() 231begin 232wait_task_entry: 233 call timed_wait_signal(); 234wait_task_exit: 235 return; 236end procedure; 237 238procedure put_task() 239begin 240put_task_lock: 241 lock(queue_lock_); 242put_task_check_active: 243 if is_active = FALSE then 244 goto put_task_exit; 245 end if; 246put_task_full_queue: 247 if is_full then 248 call wait_task(); 249 goto put_task_full_queue; 250 end if; 251put_task_increase_queue_size: 252 call add_task(); 253put_task_signal: 254 signal(cond_var_); 255put_task_exit: 256 unlock(queue_lock_); 257 return; 258end procedure; 259 260procedure try_put_task() 261begin 262try_put_task_lock: 263 lock(queue_lock_); 264try_put_task_check_active: 265 if is_active = FALSE then 266 goto try_put_task_exit; 267 end if; 268try_put_task_check_full_queue: 269 call try_add_task(); 270try_put_task_signal: 271 signal(cond_var_); 272try_put_task_exit: 273 unlock(queue_lock_); 274 return; 275end procedure; 276 277\* Processes 278 279fair process worker \in workers_set 280variable task = 0; 281begin 282worker_inactive: 283 while workers[self] = FALSE do 284 if is_active = FALSE then 285 goto worker_exit; 286 end if; 287 end while; 288worker_lock: 289 workers_status[self] := TRUE; 290 lock(queue_lock_); 291worker_check_active: 292 if workers[self] = FALSE then 293 unlock(queue_lock_); 294 goto worker_exit; 295 end if; 296worker_get_task: 297 call get_task(); 298worker_check_task_empty: 299 if task = 0 then 300 call timed_wait_signal(); 301 goto worker_unlock; 302 end if; 303worker_signal_task: 304 signal(cond_var_); 305worker_unlock: 306 unlock(queue_lock_); 307 goto worker_lock; 308worker_exit: 309 workers_status[self] := FALSE; 310end process; 311 312fair process producer \in producers_set 313begin 314producer_entry: 315 if is_active = FALSE then 316 goto producer_exit; 317 end if; 318producer_loop: 319 either goto producer_put_task; 320 or goto producer_try_put_task; 321 end either; 322producer_put_task: 323 call put_task(); 324producer_put_task_end: 325 goto producer_entry; 326producer_try_put_task: 327 call try_put_task(); 328producer_try_put_task_end: 329 goto producer_entry; 330producer_exit: 331 skip; 332end process; 333 334fair process controller \in controllers_set 335begin 336controller_loop: 337 either goto controller_scale; 338 or goto controller_shutdown; 339 or goto controller_enumerate_procs; 340 end either; 341controller_scale: 342 with n_ \in 0..max_workers do 343 call scale(n_); 344 end with; 345controller_scale_end: 346 goto controller_loop; 347controller_enumerate_procs: 348 call enumerate_procs(); 349controller_enumerate_procs_end: 350 goto controller_loop; 351controller_shutdown: 352 call shutdown(); 353controller_exit: 354 skip; 355end process; 356 357end algorithm 358 359safety(<> Finish) 360 361*) 362\* BEGIN TRANSLATION (chksum(pcal) = "c1ecf13e" /\ chksum(tla) = "e6aba2c") 363\* Parameter worker_num of procedure stop_worker at line 128 col 23 changed to worker_num_ 364CONSTANT defaultInitValue 365VARIABLES workers, workers_status, num_workers, is_active, queue_lock_, 366 scale_lock_, cond_var_, queue_size_, pc, stack 367 368(* define statement *) 369is_full == queue_size_ >= queue_max_size 370 371VARIABLES worker_num_, worker_num, num, n, task 372 373vars == << workers, workers_status, num_workers, is_active, queue_lock_, 374 scale_lock_, cond_var_, queue_size_, pc, stack, worker_num_, 375 worker_num, num, n, task >> 376 377ProcSet == (workers_set) \cup (producers_set) \cup (controllers_set) 378 379Init == (* Global variables *) 380 /\ workers = workers_initial_val 381 /\ workers_status = workers_initial_val 382 /\ num_workers = 0 383 /\ is_active = TRUE 384 /\ queue_lock_ = 0 385 /\ scale_lock_ = 0 386 /\ cond_var_ = FALSE 387 /\ queue_size_ = 0 388 (* Procedure stop_worker *) 389 /\ worker_num_ = [ self \in ProcSet |-> defaultInitValue] 390 (* Procedure create_new_thread *) 391 /\ worker_num = [ self \in ProcSet |-> defaultInitValue] 392 (* Procedure scale *) 393 /\ num = [ self \in ProcSet |-> defaultInitValue] 394 (* Procedure shutdown *) 395 /\ n = [ self \in ProcSet |-> 1] 396 (* Process worker *) 397 /\ task = [self \in workers_set |-> 0] 398 /\ stack = [self \in ProcSet |-> << >>] 399 /\ pc = [self \in ProcSet |-> CASE self \in workers_set -> "worker_inactive" 400 [] self \in producers_set -> "producer_entry" 401 [] self \in controllers_set -> "controller_loop"] 402 403timed_wait_signal_entry(self) == /\ pc[self] = "timed_wait_signal_entry" 404 /\ \/ /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_wait"] 405 \/ /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_exit"] 406 /\ UNCHANGED << workers, workers_status, 407 num_workers, is_active, 408 queue_lock_, scale_lock_, 409 cond_var_, queue_size_, stack, 410 worker_num_, worker_num, num, 411 n, task >> 412 413timed_wait_signal_wait(self) == /\ pc[self] = "timed_wait_signal_wait" 414 /\ Assert((queue_lock_ = self), 415 "Failure of assertion at line 38, column 3 of macro called at line 65, column 3.") 416 /\ queue_lock_' = 0 417 /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_wait_1"] 418 /\ UNCHANGED << workers, workers_status, 419 num_workers, is_active, 420 scale_lock_, cond_var_, 421 queue_size_, stack, 422 worker_num_, worker_num, num, 423 n, task >> 424 425timed_wait_signal_wait_1(self) == /\ pc[self] = "timed_wait_signal_wait_1" 426 /\ IF cond_var_ # TRUE \/ queue_lock_ # 0 427 THEN /\ IF is_active = FALSE 428 THEN /\ queue_lock_ = 0 429 /\ queue_lock_' = self 430 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 431 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 432 ELSE /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_wait_1"] 433 /\ UNCHANGED << queue_lock_, 434 stack >> 435 /\ UNCHANGED cond_var_ 436 ELSE /\ /\ cond_var_' = FALSE 437 /\ queue_lock_' = self 438 /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_exit"] 439 /\ stack' = stack 440 /\ UNCHANGED << workers, workers_status, 441 num_workers, is_active, 442 scale_lock_, queue_size_, 443 worker_num_, worker_num, num, 444 n, task >> 445 446timed_wait_signal_exit(self) == /\ pc[self] = "timed_wait_signal_exit" 447 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 448 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 449 /\ UNCHANGED << workers, workers_status, 450 num_workers, is_active, 451 queue_lock_, scale_lock_, 452 cond_var_, queue_size_, 453 worker_num_, worker_num, num, 454 n, task >> 455 456timed_wait_signal(self) == timed_wait_signal_entry(self) 457 \/ timed_wait_signal_wait(self) 458 \/ timed_wait_signal_wait_1(self) 459 \/ timed_wait_signal_exit(self) 460 461get_task_entry(self) == /\ pc[self] = "get_task_entry" 462 /\ IF queue_size_ = 0 463 THEN /\ task' = [task EXCEPT ![self] = 0] 464 /\ UNCHANGED queue_size_ 465 ELSE /\ task' = [task EXCEPT ![self] = 1] 466 /\ queue_size_' = queue_size_ - 1 467 /\ pc' = [pc EXCEPT ![self] = "get_task_exit"] 468 /\ UNCHANGED << workers, workers_status, num_workers, 469 is_active, queue_lock_, scale_lock_, 470 cond_var_, stack, worker_num_, 471 worker_num, num, n >> 472 473get_task_exit(self) == /\ pc[self] = "get_task_exit" 474 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 475 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 476 /\ UNCHANGED << workers, workers_status, num_workers, 477 is_active, queue_lock_, scale_lock_, 478 cond_var_, queue_size_, worker_num_, 479 worker_num, num, n, task >> 480 481get_task(self) == get_task_entry(self) \/ get_task_exit(self) 482 483add_task_increase_queue_size(self) == /\ pc[self] = "add_task_increase_queue_size" 484 /\ queue_size_' = queue_size_ + 1 485 /\ pc' = [pc EXCEPT ![self] = "add_task_exit"] 486 /\ UNCHANGED << workers, workers_status, 487 num_workers, is_active, 488 queue_lock_, scale_lock_, 489 cond_var_, stack, 490 worker_num_, worker_num, 491 num, n, task >> 492 493add_task_exit(self) == /\ pc[self] = "add_task_exit" 494 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 495 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 496 /\ UNCHANGED << workers, workers_status, num_workers, 497 is_active, queue_lock_, scale_lock_, 498 cond_var_, queue_size_, worker_num_, 499 worker_num, num, n, task >> 500 501add_task(self) == add_task_increase_queue_size(self) \/ add_task_exit(self) 502 503try_add_task_entry(self) == /\ pc[self] = "try_add_task_entry" 504 /\ IF is_full 505 THEN /\ pc' = [pc EXCEPT ![self] = "try_add_task_exit"] 506 ELSE /\ pc' = [pc EXCEPT ![self] = "try_add_task_increase_queue_size"] 507 /\ UNCHANGED << workers, workers_status, 508 num_workers, is_active, 509 queue_lock_, scale_lock_, 510 cond_var_, queue_size_, stack, 511 worker_num_, worker_num, num, n, 512 task >> 513 514try_add_task_increase_queue_size(self) == /\ pc[self] = "try_add_task_increase_queue_size" 515 /\ queue_size_' = queue_size_ + 1 516 /\ pc' = [pc EXCEPT ![self] = "try_add_task_exit"] 517 /\ UNCHANGED << workers, 518 workers_status, 519 num_workers, 520 is_active, 521 queue_lock_, 522 scale_lock_, 523 cond_var_, stack, 524 worker_num_, 525 worker_num, num, n, 526 task >> 527 528try_add_task_exit(self) == /\ pc[self] = "try_add_task_exit" 529 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 530 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 531 /\ UNCHANGED << workers, workers_status, 532 num_workers, is_active, queue_lock_, 533 scale_lock_, cond_var_, queue_size_, 534 worker_num_, worker_num, num, n, 535 task >> 536 537try_add_task(self) == try_add_task_entry(self) 538 \/ try_add_task_increase_queue_size(self) 539 \/ try_add_task_exit(self) 540 541finalize_entry(self) == /\ pc[self] = "finalize_entry" 542 /\ queue_size_' = 0 543 /\ pc' = [pc EXCEPT ![self] = "finalize_exit"] 544 /\ UNCHANGED << workers, workers_status, num_workers, 545 is_active, queue_lock_, scale_lock_, 546 cond_var_, stack, worker_num_, 547 worker_num, num, n, task >> 548 549finalize_exit(self) == /\ pc[self] = "finalize_exit" 550 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 551 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 552 /\ UNCHANGED << workers, workers_status, num_workers, 553 is_active, queue_lock_, scale_lock_, 554 cond_var_, queue_size_, worker_num_, 555 worker_num, num, n, task >> 556 557finalize(self) == finalize_entry(self) \/ finalize_exit(self) 558 559stop_worker_lock_and_signal(self) == /\ pc[self] = "stop_worker_lock_and_signal" 560 /\ queue_lock_ = 0 561 /\ queue_lock_' = self 562 /\ pc' = [pc EXCEPT ![self] = "stop_worker_finalize_queue"] 563 /\ UNCHANGED << workers, workers_status, 564 num_workers, is_active, 565 scale_lock_, cond_var_, 566 queue_size_, stack, 567 worker_num_, worker_num, 568 num, n, task >> 569 570stop_worker_finalize_queue(self) == /\ pc[self] = "stop_worker_finalize_queue" 571 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "finalize", 572 pc |-> "stop_worker_unlock" ] >> 573 \o stack[self]] 574 /\ pc' = [pc EXCEPT ![self] = "finalize_entry"] 575 /\ UNCHANGED << workers, workers_status, 576 num_workers, is_active, 577 queue_lock_, scale_lock_, 578 cond_var_, queue_size_, 579 worker_num_, worker_num, 580 num, n, task >> 581 582stop_worker_unlock(self) == /\ pc[self] = "stop_worker_unlock" 583 /\ cond_var_' = TRUE 584 /\ Assert((queue_lock_ = self), 585 "Failure of assertion at line 38, column 3 of macro called at line 136, column 3.") 586 /\ queue_lock_' = 0 587 /\ pc' = [pc EXCEPT ![self] = "stop_worker_join"] 588 /\ UNCHANGED << workers, workers_status, 589 num_workers, is_active, 590 scale_lock_, queue_size_, stack, 591 worker_num_, worker_num, num, n, 592 task >> 593 594stop_worker_join(self) == /\ pc[self] = "stop_worker_join" 595 /\ workers_status[worker_num_[self]] = FALSE 596 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 597 /\ worker_num_' = [worker_num_ EXCEPT ![self] = Head(stack[self]).worker_num_] 598 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 599 /\ UNCHANGED << workers, workers_status, num_workers, 600 is_active, queue_lock_, scale_lock_, 601 cond_var_, queue_size_, worker_num, 602 num, n, task >> 603 604stop_worker(self) == stop_worker_lock_and_signal(self) 605 \/ stop_worker_finalize_queue(self) 606 \/ stop_worker_unlock(self) 607 \/ stop_worker_join(self) 608 609create_new_thread_lock(self) == /\ pc[self] = "create_new_thread_lock" 610 /\ queue_lock_ = 0 611 /\ queue_lock_' = self 612 /\ workers' = [workers EXCEPT ![num_workers + 1] = TRUE] 613 /\ pc' = [pc EXCEPT ![self] = "create_new_thread_unlock"] 614 /\ UNCHANGED << workers_status, num_workers, 615 is_active, scale_lock_, 616 cond_var_, queue_size_, stack, 617 worker_num_, worker_num, num, 618 n, task >> 619 620create_new_thread_unlock(self) == /\ pc[self] = "create_new_thread_unlock" 621 /\ Assert((queue_lock_ = self), 622 "Failure of assertion at line 38, column 3 of macro called at line 148, column 3.") 623 /\ queue_lock_' = 0 624 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 625 /\ worker_num' = [worker_num EXCEPT ![self] = Head(stack[self]).worker_num] 626 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 627 /\ UNCHANGED << workers, workers_status, 628 num_workers, is_active, 629 scale_lock_, cond_var_, 630 queue_size_, worker_num_, 631 num, n, task >> 632 633create_new_thread(self) == create_new_thread_lock(self) 634 \/ create_new_thread_unlock(self) 635 636scale_lock(self) == /\ pc[self] = "scale_lock" 637 /\ scale_lock_ = 0 638 /\ scale_lock_' = self 639 /\ Assert(num[self] \in 0..max_workers, 640 "Failure of assertion at line 156, column 3.") 641 /\ pc' = [pc EXCEPT ![self] = "scale_check"] 642 /\ UNCHANGED << workers, workers_status, num_workers, 643 is_active, queue_lock_, cond_var_, 644 queue_size_, stack, worker_num_, 645 worker_num, num, n, task >> 646 647scale_check(self) == /\ pc[self] = "scale_check" 648 /\ IF num[self] > num_workers 649 THEN /\ pc' = [pc EXCEPT ![self] = "scale_add_workers"] 650 ELSE /\ IF num[self] < num_workers 651 THEN /\ pc' = [pc EXCEPT ![self] = "scale_del_workers"] 652 ELSE /\ pc' = [pc EXCEPT ![self] = "scale_ret"] 653 /\ UNCHANGED << workers, workers_status, num_workers, 654 is_active, queue_lock_, scale_lock_, 655 cond_var_, queue_size_, stack, 656 worker_num_, worker_num, num, n, task >> 657 658scale_add_workers(self) == /\ pc[self] = "scale_add_workers" 659 /\ IF num_workers < num[self] 660 THEN /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "create_new_thread", 661 pc |-> "scale_queue_inc_lock", 662 worker_num |-> worker_num[self] ] >> 663 \o stack[self]] 664 /\ worker_num' = [worker_num EXCEPT ![self] = num_workers] 665 /\ pc' = [pc EXCEPT ![self] = "create_new_thread_lock"] 666 ELSE /\ pc' = [pc EXCEPT ![self] = "scale_del_workers"] 667 /\ UNCHANGED << stack, worker_num >> 668 /\ UNCHANGED << workers, workers_status, 669 num_workers, is_active, queue_lock_, 670 scale_lock_, cond_var_, queue_size_, 671 worker_num_, num, n, task >> 672 673scale_queue_inc_lock(self) == /\ pc[self] = "scale_queue_inc_lock" 674 /\ queue_lock_ = 0 675 /\ queue_lock_' = self 676 /\ pc' = [pc EXCEPT ![self] = "scale_add_workers_inc"] 677 /\ UNCHANGED << workers, workers_status, 678 num_workers, is_active, 679 scale_lock_, cond_var_, 680 queue_size_, stack, worker_num_, 681 worker_num, num, n, task >> 682 683scale_add_workers_inc(self) == /\ pc[self] = "scale_add_workers_inc" 684 /\ num_workers' = num_workers + 1 685 /\ pc' = [pc EXCEPT ![self] = "scale_queue_inc_unlock"] 686 /\ UNCHANGED << workers, workers_status, 687 is_active, queue_lock_, 688 scale_lock_, cond_var_, 689 queue_size_, stack, worker_num_, 690 worker_num, num, n, task >> 691 692scale_queue_inc_unlock(self) == /\ pc[self] = "scale_queue_inc_unlock" 693 /\ Assert((queue_lock_ = self), 694 "Failure of assertion at line 38, column 3 of macro called at line 170, column 5.") 695 /\ queue_lock_' = 0 696 /\ pc' = [pc EXCEPT ![self] = "scale_add_workers"] 697 /\ UNCHANGED << workers, workers_status, 698 num_workers, is_active, 699 scale_lock_, cond_var_, 700 queue_size_, stack, 701 worker_num_, worker_num, num, 702 n, task >> 703 704scale_del_workers(self) == /\ pc[self] = "scale_del_workers" 705 /\ IF num_workers > num[self] 706 THEN /\ workers' = [workers EXCEPT ![num_workers] = FALSE] 707 /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "stop_worker", 708 pc |-> "scale_queue_dec_lock", 709 worker_num_ |-> worker_num_[self] ] >> 710 \o stack[self]] 711 /\ worker_num_' = [worker_num_ EXCEPT ![self] = num_workers] 712 /\ pc' = [pc EXCEPT ![self] = "stop_worker_lock_and_signal"] 713 ELSE /\ pc' = [pc EXCEPT ![self] = "scale_ret"] 714 /\ UNCHANGED << workers, stack, 715 worker_num_ >> 716 /\ UNCHANGED << workers_status, num_workers, 717 is_active, queue_lock_, scale_lock_, 718 cond_var_, queue_size_, worker_num, 719 num, n, task >> 720 721scale_queue_dec_lock(self) == /\ pc[self] = "scale_queue_dec_lock" 722 /\ queue_lock_ = 0 723 /\ queue_lock_' = self 724 /\ pc' = [pc EXCEPT ![self] = "scale_del_workers_dec_num_workers"] 725 /\ UNCHANGED << workers, workers_status, 726 num_workers, is_active, 727 scale_lock_, cond_var_, 728 queue_size_, stack, worker_num_, 729 worker_num, num, n, task >> 730 731scale_del_workers_dec_num_workers(self) == /\ pc[self] = "scale_del_workers_dec_num_workers" 732 /\ num_workers' = num_workers - 1 733 /\ pc' = [pc EXCEPT ![self] = "scale_queue_dec_unlock"] 734 /\ UNCHANGED << workers, 735 workers_status, 736 is_active, 737 queue_lock_, 738 scale_lock_, 739 cond_var_, 740 queue_size_, stack, 741 worker_num_, 742 worker_num, num, n, 743 task >> 744 745scale_queue_dec_unlock(self) == /\ pc[self] = "scale_queue_dec_unlock" 746 /\ Assert((queue_lock_ = self), 747 "Failure of assertion at line 38, column 3 of macro called at line 181, column 5.") 748 /\ queue_lock_' = 0 749 /\ pc' = [pc EXCEPT ![self] = "scale_del_workers"] 750 /\ UNCHANGED << workers, workers_status, 751 num_workers, is_active, 752 scale_lock_, cond_var_, 753 queue_size_, stack, 754 worker_num_, worker_num, num, 755 n, task >> 756 757scale_ret(self) == /\ pc[self] = "scale_ret" 758 /\ Assert((scale_lock_ = self), 759 "Failure of assertion at line 38, column 3 of macro called at line 184, column 3.") 760 /\ scale_lock_' = 0 761 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 762 /\ num' = [num EXCEPT ![self] = Head(stack[self]).num] 763 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 764 /\ UNCHANGED << workers, workers_status, num_workers, 765 is_active, queue_lock_, cond_var_, 766 queue_size_, worker_num_, worker_num, n, 767 task >> 768 769scale(self) == scale_lock(self) \/ scale_check(self) 770 \/ scale_add_workers(self) \/ scale_queue_inc_lock(self) 771 \/ scale_add_workers_inc(self) 772 \/ scale_queue_inc_unlock(self) 773 \/ scale_del_workers(self) \/ scale_queue_dec_lock(self) 774 \/ scale_del_workers_dec_num_workers(self) 775 \/ scale_queue_dec_unlock(self) \/ scale_ret(self) 776 777enumerate_procs_lock(self) == /\ pc[self] = "enumerate_procs_lock" 778 /\ scale_lock_ = 0 779 /\ scale_lock_' = self 780 /\ pc' = [pc EXCEPT ![self] = "enumerate_procs_unlock"] 781 /\ UNCHANGED << workers, workers_status, 782 num_workers, is_active, 783 queue_lock_, cond_var_, 784 queue_size_, stack, worker_num_, 785 worker_num, num, n, task >> 786 787enumerate_procs_unlock(self) == /\ pc[self] = "enumerate_procs_unlock" 788 /\ Assert((scale_lock_ = self), 789 "Failure of assertion at line 38, column 3 of macro called at line 193, column 3.") 790 /\ scale_lock_' = 0 791 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 792 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 793 /\ UNCHANGED << workers, workers_status, 794 num_workers, is_active, 795 queue_lock_, cond_var_, 796 queue_size_, worker_num_, 797 worker_num, num, n, task >> 798 799enumerate_procs(self) == enumerate_procs_lock(self) 800 \/ enumerate_procs_unlock(self) 801 802shutdown_lock(self) == /\ pc[self] = "shutdown_lock" 803 /\ scale_lock_ = 0 804 /\ scale_lock_' = self 805 /\ pc' = [pc EXCEPT ![self] = "shutdown_loop"] 806 /\ UNCHANGED << workers, workers_status, num_workers, 807 is_active, queue_lock_, cond_var_, 808 queue_size_, stack, worker_num_, 809 worker_num, num, n, task >> 810 811shutdown_loop(self) == /\ pc[self] = "shutdown_loop" 812 /\ IF n[self] <= num_workers 813 THEN /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "stop_worker", 814 pc |-> "shutdown_inc_n", 815 worker_num_ |-> worker_num_[self] ] >> 816 \o stack[self]] 817 /\ worker_num_' = [worker_num_ EXCEPT ![self] = n[self]] 818 /\ pc' = [pc EXCEPT ![self] = "stop_worker_lock_and_signal"] 819 ELSE /\ pc' = [pc EXCEPT ![self] = "shutdown_unlock"] 820 /\ UNCHANGED << stack, worker_num_ >> 821 /\ UNCHANGED << workers, workers_status, num_workers, 822 is_active, queue_lock_, scale_lock_, 823 cond_var_, queue_size_, worker_num, num, 824 n, task >> 825 826shutdown_inc_n(self) == /\ pc[self] = "shutdown_inc_n" 827 /\ n' = [n EXCEPT ![self] = n[self] + 1] 828 /\ pc' = [pc EXCEPT ![self] = "shutdown_loop"] 829 /\ UNCHANGED << workers, workers_status, num_workers, 830 is_active, queue_lock_, scale_lock_, 831 cond_var_, queue_size_, stack, 832 worker_num_, worker_num, num, task >> 833 834shutdown_unlock(self) == /\ pc[self] = "shutdown_unlock" 835 /\ Assert((scale_lock_ = self), 836 "Failure of assertion at line 38, column 3 of macro called at line 210, column 3.") 837 /\ scale_lock_' = 0 838 /\ pc' = [pc EXCEPT ![self] = "shutdown_exit"] 839 /\ UNCHANGED << workers, workers_status, num_workers, 840 is_active, queue_lock_, cond_var_, 841 queue_size_, stack, worker_num_, 842 worker_num, num, n, task >> 843 844shutdown_exit(self) == /\ pc[self] = "shutdown_exit" 845 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 846 /\ n' = [n EXCEPT ![self] = Head(stack[self]).n] 847 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 848 /\ UNCHANGED << workers, workers_status, num_workers, 849 is_active, queue_lock_, scale_lock_, 850 cond_var_, queue_size_, worker_num_, 851 worker_num, num, task >> 852 853shutdown(self) == shutdown_lock(self) \/ shutdown_loop(self) 854 \/ shutdown_inc_n(self) \/ shutdown_unlock(self) 855 \/ shutdown_exit(self) 856 857wait_task_entry(self) == /\ pc[self] = "wait_task_entry" 858 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "timed_wait_signal", 859 pc |-> "wait_task_exit" ] >> 860 \o stack[self]] 861 /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_entry"] 862 /\ UNCHANGED << workers, workers_status, num_workers, 863 is_active, queue_lock_, scale_lock_, 864 cond_var_, queue_size_, worker_num_, 865 worker_num, num, n, task >> 866 867wait_task_exit(self) == /\ pc[self] = "wait_task_exit" 868 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 869 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 870 /\ UNCHANGED << workers, workers_status, num_workers, 871 is_active, queue_lock_, scale_lock_, 872 cond_var_, queue_size_, worker_num_, 873 worker_num, num, n, task >> 874 875wait_task(self) == wait_task_entry(self) \/ wait_task_exit(self) 876 877put_task_lock(self) == /\ pc[self] = "put_task_lock" 878 /\ queue_lock_ = 0 879 /\ queue_lock_' = self 880 /\ pc' = [pc EXCEPT ![self] = "put_task_check_active"] 881 /\ UNCHANGED << workers, workers_status, num_workers, 882 is_active, scale_lock_, cond_var_, 883 queue_size_, stack, worker_num_, 884 worker_num, num, n, task >> 885 886put_task_check_active(self) == /\ pc[self] = "put_task_check_active" 887 /\ IF is_active = FALSE 888 THEN /\ pc' = [pc EXCEPT ![self] = "put_task_exit"] 889 ELSE /\ pc' = [pc EXCEPT ![self] = "put_task_full_queue"] 890 /\ UNCHANGED << workers, workers_status, 891 num_workers, is_active, 892 queue_lock_, scale_lock_, 893 cond_var_, queue_size_, stack, 894 worker_num_, worker_num, num, n, 895 task >> 896 897put_task_full_queue(self) == /\ pc[self] = "put_task_full_queue" 898 /\ IF is_full 899 THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "wait_task", 900 pc |-> "put_task_full_queue" ] >> 901 \o stack[self]] 902 /\ pc' = [pc EXCEPT ![self] = "wait_task_entry"] 903 ELSE /\ pc' = [pc EXCEPT ![self] = "put_task_increase_queue_size"] 904 /\ stack' = stack 905 /\ UNCHANGED << workers, workers_status, 906 num_workers, is_active, 907 queue_lock_, scale_lock_, 908 cond_var_, queue_size_, 909 worker_num_, worker_num, num, n, 910 task >> 911 912put_task_increase_queue_size(self) == /\ pc[self] = "put_task_increase_queue_size" 913 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "add_task", 914 pc |-> "put_task_signal" ] >> 915 \o stack[self]] 916 /\ pc' = [pc EXCEPT ![self] = "add_task_increase_queue_size"] 917 /\ UNCHANGED << workers, workers_status, 918 num_workers, is_active, 919 queue_lock_, scale_lock_, 920 cond_var_, queue_size_, 921 worker_num_, worker_num, 922 num, n, task >> 923 924put_task_signal(self) == /\ pc[self] = "put_task_signal" 925 /\ cond_var_' = TRUE 926 /\ pc' = [pc EXCEPT ![self] = "put_task_exit"] 927 /\ UNCHANGED << workers, workers_status, num_workers, 928 is_active, queue_lock_, scale_lock_, 929 queue_size_, stack, worker_num_, 930 worker_num, num, n, task >> 931 932put_task_exit(self) == /\ pc[self] = "put_task_exit" 933 /\ Assert((queue_lock_ = self), 934 "Failure of assertion at line 38, column 3 of macro called at line 241, column 3.") 935 /\ queue_lock_' = 0 936 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 937 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 938 /\ UNCHANGED << workers, workers_status, num_workers, 939 is_active, scale_lock_, cond_var_, 940 queue_size_, worker_num_, worker_num, 941 num, n, task >> 942 943put_task(self) == put_task_lock(self) \/ put_task_check_active(self) 944 \/ put_task_full_queue(self) 945 \/ put_task_increase_queue_size(self) 946 \/ put_task_signal(self) \/ put_task_exit(self) 947 948try_put_task_lock(self) == /\ pc[self] = "try_put_task_lock" 949 /\ queue_lock_ = 0 950 /\ queue_lock_' = self 951 /\ pc' = [pc EXCEPT ![self] = "try_put_task_check_active"] 952 /\ UNCHANGED << workers, workers_status, 953 num_workers, is_active, scale_lock_, 954 cond_var_, queue_size_, stack, 955 worker_num_, worker_num, num, n, 956 task >> 957 958try_put_task_check_active(self) == /\ pc[self] = "try_put_task_check_active" 959 /\ IF is_active = FALSE 960 THEN /\ pc' = [pc EXCEPT ![self] = "try_put_task_exit"] 961 ELSE /\ pc' = [pc EXCEPT ![self] = "try_put_task_check_full_queue"] 962 /\ UNCHANGED << workers, workers_status, 963 num_workers, is_active, 964 queue_lock_, scale_lock_, 965 cond_var_, queue_size_, 966 stack, worker_num_, 967 worker_num, num, n, task >> 968 969try_put_task_check_full_queue(self) == /\ pc[self] = "try_put_task_check_full_queue" 970 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "try_add_task", 971 pc |-> "try_put_task_signal" ] >> 972 \o stack[self]] 973 /\ pc' = [pc EXCEPT ![self] = "try_add_task_entry"] 974 /\ UNCHANGED << workers, workers_status, 975 num_workers, is_active, 976 queue_lock_, 977 scale_lock_, cond_var_, 978 queue_size_, 979 worker_num_, worker_num, 980 num, n, task >> 981 982try_put_task_signal(self) == /\ pc[self] = "try_put_task_signal" 983 /\ cond_var_' = TRUE 984 /\ pc' = [pc EXCEPT ![self] = "try_put_task_exit"] 985 /\ UNCHANGED << workers, workers_status, 986 num_workers, is_active, 987 queue_lock_, scale_lock_, 988 queue_size_, stack, worker_num_, 989 worker_num, num, n, task >> 990 991try_put_task_exit(self) == /\ pc[self] = "try_put_task_exit" 992 /\ Assert((queue_lock_ = self), 993 "Failure of assertion at line 38, column 3 of macro called at line 258, column 3.") 994 /\ queue_lock_' = 0 995 /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc] 996 /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])] 997 /\ UNCHANGED << workers, workers_status, 998 num_workers, is_active, scale_lock_, 999 cond_var_, queue_size_, worker_num_, 1000 worker_num, num, n, task >> 1001 1002try_put_task(self) == try_put_task_lock(self) 1003 \/ try_put_task_check_active(self) 1004 \/ try_put_task_check_full_queue(self) 1005 \/ try_put_task_signal(self) 1006 \/ try_put_task_exit(self) 1007 1008worker_inactive(self) == /\ pc[self] = "worker_inactive" 1009 /\ IF workers[self] = FALSE 1010 THEN /\ IF is_active = FALSE 1011 THEN /\ pc' = [pc EXCEPT ![self] = "worker_exit"] 1012 ELSE /\ pc' = [pc EXCEPT ![self] = "worker_inactive"] 1013 ELSE /\ pc' = [pc EXCEPT ![self] = "worker_lock"] 1014 /\ UNCHANGED << workers, workers_status, num_workers, 1015 is_active, queue_lock_, scale_lock_, 1016 cond_var_, queue_size_, stack, 1017 worker_num_, worker_num, num, n, task >> 1018 1019worker_lock(self) == /\ pc[self] = "worker_lock" 1020 /\ workers_status' = [workers_status EXCEPT ![self] = TRUE] 1021 /\ queue_lock_ = 0 1022 /\ queue_lock_' = self 1023 /\ pc' = [pc EXCEPT ![self] = "worker_check_active"] 1024 /\ UNCHANGED << workers, num_workers, is_active, 1025 scale_lock_, cond_var_, queue_size_, 1026 stack, worker_num_, worker_num, num, n, 1027 task >> 1028 1029worker_check_active(self) == /\ pc[self] = "worker_check_active" 1030 /\ IF workers[self] = FALSE 1031 THEN /\ Assert((queue_lock_ = self), 1032 "Failure of assertion at line 38, column 3 of macro called at line 278, column 5.") 1033 /\ queue_lock_' = 0 1034 /\ pc' = [pc EXCEPT ![self] = "worker_exit"] 1035 ELSE /\ pc' = [pc EXCEPT ![self] = "worker_get_task"] 1036 /\ UNCHANGED queue_lock_ 1037 /\ UNCHANGED << workers, workers_status, 1038 num_workers, is_active, 1039 scale_lock_, cond_var_, 1040 queue_size_, stack, worker_num_, 1041 worker_num, num, n, task >> 1042 1043worker_get_task(self) == /\ pc[self] = "worker_get_task" 1044 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "get_task", 1045 pc |-> "worker_check_task_empty" ] >> 1046 \o stack[self]] 1047 /\ pc' = [pc EXCEPT ![self] = "get_task_entry"] 1048 /\ UNCHANGED << workers, workers_status, num_workers, 1049 is_active, queue_lock_, scale_lock_, 1050 cond_var_, queue_size_, worker_num_, 1051 worker_num, num, n, task >> 1052 1053worker_check_task_empty(self) == /\ pc[self] = "worker_check_task_empty" 1054 /\ IF task[self] = 0 1055 THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "timed_wait_signal", 1056 pc |-> "worker_unlock" ] >> 1057 \o stack[self]] 1058 /\ pc' = [pc EXCEPT ![self] = "timed_wait_signal_entry"] 1059 ELSE /\ pc' = [pc EXCEPT ![self] = "worker_signal_task"] 1060 /\ stack' = stack 1061 /\ UNCHANGED << workers, workers_status, 1062 num_workers, is_active, 1063 queue_lock_, scale_lock_, 1064 cond_var_, queue_size_, 1065 worker_num_, worker_num, num, 1066 n, task >> 1067 1068worker_signal_task(self) == /\ pc[self] = "worker_signal_task" 1069 /\ cond_var_' = TRUE 1070 /\ pc' = [pc EXCEPT ![self] = "worker_unlock"] 1071 /\ UNCHANGED << workers, workers_status, 1072 num_workers, is_active, 1073 queue_lock_, scale_lock_, 1074 queue_size_, stack, worker_num_, 1075 worker_num, num, n, task >> 1076 1077worker_unlock(self) == /\ pc[self] = "worker_unlock" 1078 /\ Assert((queue_lock_ = self), 1079 "Failure of assertion at line 38, column 3 of macro called at line 291, column 3.") 1080 /\ queue_lock_' = 0 1081 /\ pc' = [pc EXCEPT ![self] = "worker_lock"] 1082 /\ UNCHANGED << workers, workers_status, num_workers, 1083 is_active, scale_lock_, cond_var_, 1084 queue_size_, stack, worker_num_, 1085 worker_num, num, n, task >> 1086 1087worker_exit(self) == /\ pc[self] = "worker_exit" 1088 /\ workers_status' = [workers_status EXCEPT ![self] = FALSE] 1089 /\ pc' = [pc EXCEPT ![self] = "Done"] 1090 /\ UNCHANGED << workers, num_workers, is_active, 1091 queue_lock_, scale_lock_, cond_var_, 1092 queue_size_, stack, worker_num_, 1093 worker_num, num, n, task >> 1094 1095worker(self) == worker_inactive(self) \/ worker_lock(self) 1096 \/ worker_check_active(self) \/ worker_get_task(self) 1097 \/ worker_check_task_empty(self) 1098 \/ worker_signal_task(self) \/ worker_unlock(self) 1099 \/ worker_exit(self) 1100 1101producer_entry(self) == /\ pc[self] = "producer_entry" 1102 /\ IF is_active = FALSE 1103 THEN /\ pc' = [pc EXCEPT ![self] = "producer_exit"] 1104 ELSE /\ pc' = [pc EXCEPT ![self] = "producer_loop"] 1105 /\ UNCHANGED << workers, workers_status, num_workers, 1106 is_active, queue_lock_, scale_lock_, 1107 cond_var_, queue_size_, stack, 1108 worker_num_, worker_num, num, n, task >> 1109 1110producer_loop(self) == /\ pc[self] = "producer_loop" 1111 /\ \/ /\ pc' = [pc EXCEPT ![self] = "producer_put_task"] 1112 \/ /\ pc' = [pc EXCEPT ![self] = "producer_try_put_task"] 1113 /\ UNCHANGED << workers, workers_status, num_workers, 1114 is_active, queue_lock_, scale_lock_, 1115 cond_var_, queue_size_, stack, 1116 worker_num_, worker_num, num, n, task >> 1117 1118producer_put_task(self) == /\ pc[self] = "producer_put_task" 1119 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "put_task", 1120 pc |-> "producer_put_task_end" ] >> 1121 \o stack[self]] 1122 /\ pc' = [pc EXCEPT ![self] = "put_task_lock"] 1123 /\ UNCHANGED << workers, workers_status, 1124 num_workers, is_active, queue_lock_, 1125 scale_lock_, cond_var_, queue_size_, 1126 worker_num_, worker_num, num, n, 1127 task >> 1128 1129producer_put_task_end(self) == /\ pc[self] = "producer_put_task_end" 1130 /\ pc' = [pc EXCEPT ![self] = "producer_entry"] 1131 /\ UNCHANGED << workers, workers_status, 1132 num_workers, is_active, 1133 queue_lock_, scale_lock_, 1134 cond_var_, queue_size_, stack, 1135 worker_num_, worker_num, num, n, 1136 task >> 1137 1138producer_try_put_task(self) == /\ pc[self] = "producer_try_put_task" 1139 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "try_put_task", 1140 pc |-> "producer_try_put_task_end" ] >> 1141 \o stack[self]] 1142 /\ pc' = [pc EXCEPT ![self] = "try_put_task_lock"] 1143 /\ UNCHANGED << workers, workers_status, 1144 num_workers, is_active, 1145 queue_lock_, scale_lock_, 1146 cond_var_, queue_size_, 1147 worker_num_, worker_num, num, n, 1148 task >> 1149 1150producer_try_put_task_end(self) == /\ pc[self] = "producer_try_put_task_end" 1151 /\ pc' = [pc EXCEPT ![self] = "producer_entry"] 1152 /\ UNCHANGED << workers, workers_status, 1153 num_workers, is_active, 1154 queue_lock_, scale_lock_, 1155 cond_var_, queue_size_, 1156 stack, worker_num_, 1157 worker_num, num, n, task >> 1158 1159producer_exit(self) == /\ pc[self] = "producer_exit" 1160 /\ TRUE 1161 /\ pc' = [pc EXCEPT ![self] = "Done"] 1162 /\ UNCHANGED << workers, workers_status, num_workers, 1163 is_active, queue_lock_, scale_lock_, 1164 cond_var_, queue_size_, stack, 1165 worker_num_, worker_num, num, n, task >> 1166 1167producer(self) == producer_entry(self) \/ producer_loop(self) 1168 \/ producer_put_task(self) 1169 \/ producer_put_task_end(self) 1170 \/ producer_try_put_task(self) 1171 \/ producer_try_put_task_end(self) 1172 \/ producer_exit(self) 1173 1174controller_loop(self) == /\ pc[self] = "controller_loop" 1175 /\ \/ /\ pc' = [pc EXCEPT ![self] = "controller_scale"] 1176 \/ /\ pc' = [pc EXCEPT ![self] = "controller_shutdown"] 1177 \/ /\ pc' = [pc EXCEPT ![self] = "controller_enumerate_procs"] 1178 /\ UNCHANGED << workers, workers_status, num_workers, 1179 is_active, queue_lock_, scale_lock_, 1180 cond_var_, queue_size_, stack, 1181 worker_num_, worker_num, num, n, task >> 1182 1183controller_scale(self) == /\ pc[self] = "controller_scale" 1184 /\ \E n_ \in 0..max_workers: 1185 /\ /\ num' = [num EXCEPT ![self] = n_] 1186 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "scale", 1187 pc |-> "controller_scale_end", 1188 num |-> num[self] ] >> 1189 \o stack[self]] 1190 /\ pc' = [pc EXCEPT ![self] = "scale_lock"] 1191 /\ UNCHANGED << workers, workers_status, num_workers, 1192 is_active, queue_lock_, scale_lock_, 1193 cond_var_, queue_size_, worker_num_, 1194 worker_num, n, task >> 1195 1196controller_scale_end(self) == /\ pc[self] = "controller_scale_end" 1197 /\ pc' = [pc EXCEPT ![self] = "controller_loop"] 1198 /\ UNCHANGED << workers, workers_status, 1199 num_workers, is_active, 1200 queue_lock_, scale_lock_, 1201 cond_var_, queue_size_, stack, 1202 worker_num_, worker_num, num, n, 1203 task >> 1204 1205controller_enumerate_procs(self) == /\ pc[self] = "controller_enumerate_procs" 1206 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "enumerate_procs", 1207 pc |-> "controller_enumerate_procs_end" ] >> 1208 \o stack[self]] 1209 /\ pc' = [pc EXCEPT ![self] = "enumerate_procs_lock"] 1210 /\ UNCHANGED << workers, workers_status, 1211 num_workers, is_active, 1212 queue_lock_, scale_lock_, 1213 cond_var_, queue_size_, 1214 worker_num_, worker_num, 1215 num, n, task >> 1216 1217controller_enumerate_procs_end(self) == /\ pc[self] = "controller_enumerate_procs_end" 1218 /\ pc' = [pc EXCEPT ![self] = "controller_loop"] 1219 /\ UNCHANGED << workers, 1220 workers_status, 1221 num_workers, is_active, 1222 queue_lock_, 1223 scale_lock_, cond_var_, 1224 queue_size_, stack, 1225 worker_num_, 1226 worker_num, num, n, 1227 task >> 1228 1229controller_shutdown(self) == /\ pc[self] = "controller_shutdown" 1230 /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "shutdown", 1231 pc |-> "controller_exit", 1232 n |-> n[self] ] >> 1233 \o stack[self]] 1234 /\ n' = [n EXCEPT ![self] = 1] 1235 /\ pc' = [pc EXCEPT ![self] = "shutdown_lock"] 1236 /\ UNCHANGED << workers, workers_status, 1237 num_workers, is_active, 1238 queue_lock_, scale_lock_, 1239 cond_var_, queue_size_, 1240 worker_num_, worker_num, num, 1241 task >> 1242 1243controller_exit(self) == /\ pc[self] = "controller_exit" 1244 /\ TRUE 1245 /\ pc' = [pc EXCEPT ![self] = "Done"] 1246 /\ UNCHANGED << workers, workers_status, num_workers, 1247 is_active, queue_lock_, scale_lock_, 1248 cond_var_, queue_size_, stack, 1249 worker_num_, worker_num, num, n, task >> 1250 1251controller(self) == controller_loop(self) \/ controller_scale(self) 1252 \/ controller_scale_end(self) 1253 \/ controller_enumerate_procs(self) 1254 \/ controller_enumerate_procs_end(self) 1255 \/ controller_shutdown(self) 1256 \/ controller_exit(self) 1257 1258(* Allow infinite stuttering to prevent deadlock on termination. *) 1259Terminating == /\ \A self \in ProcSet: pc[self] = "Done" 1260 /\ UNCHANGED vars 1261 1262Next == (\E self \in ProcSet: \/ timed_wait_signal(self) \/ get_task(self) 1263 \/ add_task(self) \/ try_add_task(self) 1264 \/ finalize(self) \/ stop_worker(self) 1265 \/ create_new_thread(self) \/ scale(self) 1266 \/ enumerate_procs(self) \/ shutdown(self) 1267 \/ wait_task(self) \/ put_task(self) 1268 \/ try_put_task(self)) 1269 \/ (\E self \in workers_set: worker(self)) 1270 \/ (\E self \in producers_set: producer(self)) 1271 \/ (\E self \in controllers_set: controller(self)) 1272 \/ Terminating 1273 1274Spec == /\ Init /\ [][Next]_vars 1275 /\ \A self \in workers_set : /\ WF_vars(worker(self)) 1276 /\ WF_vars(get_task(self)) 1277 /\ WF_vars(timed_wait_signal(self)) 1278 /\ \A self \in producers_set : /\ WF_vars(producer(self)) 1279 /\ WF_vars(put_task(self)) 1280 /\ WF_vars(try_put_task(self)) 1281 /\ WF_vars(timed_wait_signal(self)) 1282 /\ WF_vars(add_task(self)) 1283 /\ WF_vars(wait_task(self)) 1284 /\ WF_vars(try_add_task(self)) 1285 /\ \A self \in controllers_set : /\ WF_vars(controller(self)) 1286 /\ WF_vars(scale(self)) 1287 /\ WF_vars(enumerate_procs(self)) 1288 /\ WF_vars(shutdown(self)) 1289 /\ WF_vars(finalize(self)) 1290 /\ WF_vars(stop_worker(self)) 1291 /\ WF_vars(create_new_thread(self)) 1292 1293Termination == <>(\A self \in ProcSet: pc[self] = "Done") 1294 1295\* END TRANSLATION 1296 1297============================================================================= 1298