우리는 fork-join 프로그램의 병렬 시간 복잡도를 검증하기 위한 동시성 분리 논리인 Parcas를 제시합니다. 기계의 세부 사항으로부터 추상화하기 위해, 병렬 프로그램의 시간 복잡도는 두 가지 측정 기준, 즉 총 연산 횟수를 측정하는 작업(work)과 가장 긴 순차적 의존 체인을 측정하는 전파 시간(span)이라는 용어로 주어집니다. 이 두 측정 기준은 함께 임의의 수의 프로세서에서 실행 시간을 결정합니다. 작업과 전파 시간에 대한 경계를 증명하기 위해, Parcas는 비용을 발생시킬 권한을 나타내는 논리적 장치인 작업 크레딧(work credits)과 전파 시간 크레딧(span credits)을 갖추고 있습니다. 작업 크레딧은 순차 프로그램의 시간 복잡도를 제한하는 표준 도구인 시간 크레딧(time credits)의 간단한 적응이며, 병렬 태스크 간에 가산적으로 분할될 수 있습니다. 그러나 전파 시간 크레딧은 근본적으로 다른 처리가 필요합니다. 실제로 두 태스크의 병렬 합성의 전파 시간은 두 태스크 전파 시간의 최댓값입니다. 이를 설명하기 위해, 우리는 fork 지점에서 전파 시간 크레딧을 복제하는 규칙을 제안하며, 각 사본에는 어떤 태스크가 이 크레딧을 사용할 수 있는지 제한하는 논리적 태스크 식별자로 태그가 지정됩니다. 전송 규칙(transfer rule)은 사용되지 않은 전파 시간 크레딧이 순차 합성(sequential compositions)을 통해 후속 태스크로 전달될 수 있도록 허용합니다. 이 논리는 병렬 for 루프나 tabulate 함수와 같은 일반적인 병렬 기본 요소에 대해 모듈식의 고계어 사양(higher-order specifications)을 제공할 만큼 충분히 표현력이 풍부합니다. 우리는 병렬 접두사 합(parallel prefix sums), 병렬 병합 정렬(parallel merge sort), 그리고 동시성과 병렬성을 혼합한 Treiber의 락 프리 스택 변형을 포함하여 여러 사례 연구에서 Parcas를 시연합니다. 제시된 모든 결과는 Iris 분리 논리 프레임워크를 사용하는 Rocq prover를 사용하여 기계화되었습니다.